let p, q, r be Element of (Formal-Series L); :: according to VECTSP_1:def 3 :: thesis: (q + r) * p = (q * p) + (r * p)
reconsider p1 = p, q1 = q, r1 = r as sequence of L by Def2;
A2: ( q * p = q1 *' p1 & r * p = r1 *' p1 ) by Def2;
q + r = q1 + r1 by Def2;
hence (q + r) * p = (q1 + r1) *' p1 by Def2
.= (q1 *' p1) + (r1 *' p1) by POLYNOM3:32
.= (q * p) + (r * p) by A2, Def2 ;
:: thesis: verum