let p, q, r be Element of (Polynom-Ring L); :: according to VECTSP_1:def 7 :: thesis: ( p * (q + r) = (p * q) + (p * r) & (q + r) * p = (q * p) + (r * p) )

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

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

q + r = q1 + r1 by Def10;

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

.= (p1 *' q1) + (p1 *' r1) by Th29

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

:: thesis: (q + r) * p = (q * p) + (r * p)

A2: ( q * p = q1 *' p1 & r * p = r1 *' p1 ) by Def10;

q + r = q1 + r1 by Def10;

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

.= (q1 *' p1) + (r1 *' p1) by Th30

.= (q * p) + (r * p) by A2, Def10 ;

:: thesis: verum

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

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

q + r = q1 + r1 by Def10;

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

.= (p1 *' q1) + (p1 *' r1) by Th29

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

:: thesis: (q + r) * p = (q * p) + (r * p)

A2: ( q * p = q1 *' p1 & r * p = r1 *' p1 ) by Def10;

q + r = q1 + r1 by Def10;

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

.= (q1 *' p1) + (r1 *' p1) by Th30

.= (q * p) + (r * p) by A2, Def10 ;

:: thesis: verum