List of theorems referencing the symbol DOT_RAS_MINUS

(693) Theorem 542: ({F,G} •incin RaCauchy) •imp (((F •Ras_MINUS G) in RaCauchy) & ((F •Ras_TIMES G) in RaCauchy))
(721) Theorem 570: [0 is right subtractive identity for rational sequence subtraction] (X in RaSeq) •imp (X •Ras_MINUS Ra0Seq = X)
(725) Theorem 574: [A rational sequence minus itself gives 0] (X in RaSeq) •imp ((X •Ras_MINUS X) = Ra0Seq)
(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))))