let n be set ; :: thesis: for L being non empty left-distributive doubleLoopStr
for p being Series of n,L
for a, a9 being Element of L holds (a * p) + (a9 * p) = (a + a9) * p
let L be non empty left-distributive doubleLoopStr ; :: thesis: for p being Series of n,L
for a, a9 being Element of L holds (a * p) + (a9 * p) = (a + a9) * p
let p be Series of n,L; :: thesis: for a, a9 being Element of L holds (a * p) + (a9 * p) = (a + a9) * p
let a, a9 be Element of L; :: thesis: (a * p) + (a9 * p) = (a + a9) * p
set p1 = (a * p) + (a9 * p);
set p2 = (a + a9) * p;

A1: now :: thesis: for u being object st u in dom ((a * p) + (a9 * p)) holds
((a * p) + (a9 * p)) . u = ((a + a9) * p) . u

let u be object ; :: thesis: ( u in dom ((a * p) + (a9 * p)) implies ((a * p) + (a9 * p)) . u = ((a + a9) * p) . u )
assume u in dom ((a * p) + (a9 * p)) ; :: thesis: ((a * p) + (a9 * p)) . u = ((a + a9) * p) . u
then reconsider u9 = u as bag of n ;
((a * p) + (a9 * p)) . u9 = ((a * p) . u9) + ((a9 * p) . u9) by POLYNOM1:15
.= (a * (p . u9)) + ((a9 * p) . u9) by POLYNOM7:def 9
.= (a * (p . u9)) + (a9 * (p . u9)) by POLYNOM7:def 9
.= (a + a9) * (p . u9) by VECTSP_1:def 3
.= ((a + a9) * p) . u9 by POLYNOM7:def 9 ;
hence ((a * p) + (a9 * p)) . u = ((a + a9) * p) . u ; :: thesis: verum

end;

dom ((a * p) + (a9 * p)) = Bags n by FUNCT_2:def 1
.= dom ((a + a9) * p) by FUNCT_2:def 1 ;
hence (a * p) + (a9 * p) = (a + a9) * p by A1, FUNCT_1:2; :: thesis: verum