let L be non empty right-distributive doubleLoopStr ; :: thesis: for p1, p2 being Polynomial of L
for x being Element of L holds x * (p1 + p2) = (x * p1) + (x * p2)
let p1, p2 be Polynomial of L; :: thesis: for x being Element of L holds x * (p1 + p2) = (x * p1) + (x * p2)
let x be Element of L; :: thesis: x * (p1 + p2) = (x * p1) + (x * p2)
set f = x * (p1 + p2);
set g = (x * p1) + (x * p2);

A1: now :: thesis: for i9 being object st i9 in dom (x * (p1 + p2)) holds
(x * (p1 + p2)) . i9 = ((x * p1) + (x * p2)) . i9

let i9 be object ; :: thesis: ( i9 in dom (x * (p1 + p2)) implies (x * (p1 + p2)) . i9 = ((x * p1) + (x * p2)) . i9 )
assume i9 in dom (x * (p1 + p2)) ; :: thesis: (x * (p1 + p2)) . i9 = ((x * p1) + (x * p2)) . i9
then reconsider i = i9 as Element of NAT ;
(x * (p1 + p2)) . i = x * ((p1 + p2) . i) by POLYNOM5:def 4
.= x * ((p1 . i) + (p2 . i)) by NORMSP_1:def 2
.= (x * (p1 . i)) + (x * (p2 . i)) by VECTSP_1:def 2
.= ((x * p1) . i) + (x * (p2 . i)) by POLYNOM5:def 4
.= ((x * p1) . i) + ((x * p2) . i) by POLYNOM5:def 4
.= ((x * p1) + (x * p2)) . i by NORMSP_1:def 2 ;
hence (x * (p1 + p2)) . i9 = ((x * p1) + (x * p2)) . i9 ; :: thesis: verum

end;

dom (x * (p1 + p2)) = NAT by FUNCT_2:def 1
.= dom ((x * p1) + (x * p2)) by FUNCT_2:def 1 ;
hence x * (p1 + p2) = (x * p1) + (x * p2) by A1, FUNCT_1:2; :: thesis: verum