let n be set ; :: thesis: for L being non empty left-distributive doubleLoopStr
for p being Series of n,L
for a, a' being Element of L holds (a * p) + (a' * p) = (a + a') * p
let L be non empty left-distributive doubleLoopStr ; :: thesis: for p being Series of n,L
for a, a' being Element of L holds (a * p) + (a' * p) = (a + a') * p
let p be Series of n,L; :: thesis: for a, a' being Element of L holds (a * p) + (a' * p) = (a + a') * p
let a, a' be Element of L; :: thesis: (a * p) + (a' * p) = (a + a') * p
set p1 = (a * p) + (a' * p);
set p2 = (a + a') * p;
A1: dom ((a * p) + (a' * p)) = Bags n by FUNCT_2:def 1
.= dom ((a + a') * p) by FUNCT_2:def 1 ;

now

let u be set ; :: thesis: ( u in dom ((a * p) + (a' * p)) implies ((a * p) + (a' * p)) . u = ((a + a') * p) . u )
assume u in dom ((a * p) + (a' * p)) ; :: thesis: ((a * p) + (a' * p)) . u = ((a + a') * p) . u
then reconsider u' = u as bag of by POLYNOM1:def 14;
((a * p) + (a' * p)) . u' = ((a * p) . u') + ((a' * p) . u') by POLYNOM1:def 21
.= (a * (p . u')) + ((a' * p) . u') by POLYNOM7:def 10
.= (a * (p . u')) + (a' * (p . u')) by POLYNOM7:def 10
.= (a + a') * (p . u') by VECTSP_1:def 12
.= ((a + a') * p) . u' by POLYNOM7:def 10 ;
hence ((a * p) + (a' * p)) . u = ((a + a') * p) . u ; :: thesis: verum

end;

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