let p, q, r be Element of (Formal-Series L); :: according to VECTSP_1:def 2 :: thesis: p * (q + r) = (p * q) + (p * r)

reconsider p1 = p, q1 = q, r1 = r as sequence of L by Def2;

A1: ( p * q = p1 *' q1 & p * r = p1 *' r1 ) by Def2;

q + r = q1 + r1 by Def2;

hence p * (q + r) = p1 *' (q1 + r1) by Def2

.= (p1 *' q1) + (p1 *' r1) by POLYNOM3:31

.= (p * q) + (p * r) by A1, Def2 ;

:: thesis: verum

reconsider p1 = p, q1 = q, r1 = r as sequence of L by Def2;

A1: ( p * q = p1 *' q1 & p * r = p1 *' r1 ) by Def2;

q + r = q1 + r1 by Def2;

hence p * (q + r) = p1 *' (q1 + r1) by Def2

.= (p1 *' q1) + (p1 *' r1) by POLYNOM3:31

.= (p * q) + (p * r) by A1, Def2 ;

:: thesis: verum