List of theorems referencing the symbol DOT_RES_TIMES
(878) Theorem 723: [The elementary operations on reals map Cauchy sequences into Cauchy sequences] ((F in ReCauchy) & (G in ReCauchy) & (Fp in RaCauchy) & (Gp in RaCauchy) & Ra_apseq(F,Fp) & Ra_apseq(G,Gp)) •imp ((((F •Res_PLUS G in ReCauchy) & Ra_apseq(F •Res_PLUS G,Fp •Ras_PLUS Gp))) & (((F •Res_MINUS G in ReCauchy) & Ra_apseq(F •Res_MINUS G,Fp •Ras_MINUS Gp))) & (((F •Res_TIMES G in ReCauchy) & Ra_apseq(F •Res_TIMES G,Fp •Ras_TIMES Gp))))
(881) Theorem 726: [The limit of a product is the product of limits] ((F in ReCauchy) & (G in ReCauchy)) •imp (limit(F •Res_TIMES G) = limit(F) •R_TIMES limit(G))
(905) Theorem 750: [The pointwise sum and product of two real continuous functions on two sets is continuous on their intersection] (Cf_RR(F,S) & Cf_RR(G,S2)) •imp (Cf_RR(F •Res_PLUS G,S * S2) & Cf_RR(F •Res_TIMES G,S * S2))