let L be non empty left-distributive doubleLoopStr ; :: thesis: for p being Polynomial of L
for x1, x2 being Element of L holds (x1 + x2) * p = (x1 * p) + (x2 * p)
let p be Polynomial of L; :: thesis: for x1, x2 being Element of L holds (x1 + x2) * p = (x1 * p) + (x2 * p)
let x1, x2 be Element of L; :: thesis: (x1 + x2) * p = (x1 * p) + (x2 * p)
set f = (x1 + x2) * p;
set g = (x1 * p) + (x2 * p);

A1: now :: thesis: for i9 being object st i9 in dom ((x1 + x2) * p) holds
((x1 + x2) * p) . i9 = ((x1 * p) + (x2 * p)) . i9

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

end;

dom ((x1 + x2) * p) = NAT by FUNCT_2:def 1
.= dom ((x1 * p) + (x2 * p)) by FUNCT_2:def 1 ;
hence (x1 + x2) * p = (x1 * p) + (x2 * p) by A1, FUNCT_1:2; :: thesis: verum