List of theorems referencing the symbol DOT_F_PLUS

(903) Theorem 748: ((F in Fin_Seqs(Re)) & (G in Fin_Seqs(Re))) •imp (((PolFcn(F) •F_PLUS PolFcn(G)) = PolFcn(F •PolPlus G)) & ((PolFcn(F) •F_MINUS PolFcn(G)) = PolFcn(F •PolMinus G)) & ((PolFcn(F) •F_TIMES PolFcn(G)) = PolFcn(F •PolTimes G)))
(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)
(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)
(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))