List of theorems referencing the symbol DOT_F_TIMES

(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)))
(951) Theorem 20008: ((N in RF) & (M in RF)) •imp (N •F_TIMES M = M •F_TIMES N)
(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))