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: dom ((x1 + x2) * p) = NAT by FUNCT_2:def 1
.= dom ((x1 * p) + (x2 * p)) by FUNCT_2:def 1 ;

now

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

end;

hence (x1 + x2) * p = (x1 * p) + (x2 * p) by A1, FUNCT_1:9; :: thesis: verum