List of theorems referencing the symbol RF

(949) Theorem 20006: ((N in RF) & (M in RF)) •imp (N •F_PLUS M = M •F_PLUS N)
(950) Theorem 20007: ((N in RF) & (M in RF)) •imp (N •F_PLUS M = M •F_PLUS N)
(951) Theorem 20008: ((N in RF) & (M in RF)) •imp (N •F_TIMES M = M •F_TIMES N)
(952) Theorem 20009: ((K in RF) & (N in RF) & (M in RF)) •imp (N •F_PLUS (M •F_PLUS K) = (N •F_PLUS M) •F_PLUS K)
(953) Theorem 20010: ((K in RF) & (N in RF) & (M in RF)) •imp (N •F_TIMES (M •F_TIMES K) = (N •F_TIMES M) •F_TIMES K)
(954) Theorem 20011: ((K in RF) & (N in RF) & (M in RF)) •imp (N •F_TIMES (M •F_PLUS K) = (N •F_TIMES M) •F_PLUS (N •F_TIMES K))
(955) Theorem real_function_sigma: (Svm(ser) & (range(ser) •incin RF) & Finite(ser)) •imp ((FSig(ser) in RF & (p in ser) •imp (Sig({p}) = ser(car(p)))) &(FORALL a | Sig(ser) = Sig(ser •ON (domain(ser) * a)) •R_PLUS Sig(ser •ON domain(ser) - a)))