let n be Ordinal; :: thesis: for L being non empty right_complementable Abelian add-associative right_zeroed associative distributive doubleLoopStr
for p, q, r being Series of n,L holds (p + q) *' r = (p *' r) + (q *' r)

let L be non empty right_complementable Abelian add-associative right_zeroed associative distributive doubleLoopStr ; :: thesis: for p, q, r being Series of n,L holds (p + q) *' r = (p *' r) + (q *' r)
let p, q, r be Series of n,L; :: thesis: (p + q) *' r = (p *' r) + (q *' r)
set cL = the carrier of L;
now :: thesis: for b being Element of Bags n holds ((p + q) *' r) . b = ((p *' r) + (q *' r)) . b
let b be Element of Bags n; :: thesis: ((p + q) *' r) . b = ((p *' r) + (q *' r)) . b
consider s being FinSequence of the carrier of L such that
A1: ((p + q) *' r) . b = Sum s and
A2: len s = len () and
A3: for k being Element of NAT st k in dom s holds
ex b1, b2 being bag of n st
( () /. k = <*b1,b2*> & s /. k = ((p + q) . b1) * (r . b2) ) by POLYNOM1:def 10;
consider u being FinSequence of the carrier of L such that
A4: (q *' r) . b = Sum u and
A5: len u = len () and
A6: for k being Element of NAT st k in dom u holds
ex b1, b2 being bag of n st
( () /. k = <*b1,b2*> & u /. k = (q . b1) * (r . b2) ) by POLYNOM1:def 10;
consider t being FinSequence of the carrier of L such that
A7: (p *' r) . b = Sum t and
A8: len t = len () and
A9: for k being Element of NAT st k in dom t holds
ex b1, b2 being bag of n st
( () /. k = <*b1,b2*> & t /. k = (p . b1) * (r . b2) ) by POLYNOM1:def 10;
reconsider t = t, u = u as Element of (len s) -tuples_on the carrier of L by ;
A10: dom u = dom s by ;
A11: dom t = dom s by ;
then A12: dom (t + u) = dom s by ;
A13: now :: thesis: for i being Nat st i in dom s holds
s . i = (t + u) . i
let i be Nat; :: thesis: ( i in dom s implies s . i = (t + u) . i )
assume A14: i in dom s ; :: thesis: s . i = (t + u) . i
then consider sb1, sb2 being bag of n such that
A15: (decomp b) /. i = <*sb1,sb2*> and
A16: s /. i = ((p + q) . sb1) * (r . sb2) by A3;
A17: ( t /. i = t . i & u /. i = u . i ) by ;
consider ub1, ub2 being bag of n such that
A18: (decomp b) /. i = <*ub1,ub2*> and
A19: u /. i = (q . ub1) * (r . ub2) by A6, A10, A14;
A20: ( sb1 = ub1 & sb2 = ub2 ) by ;
consider tb1, tb2 being bag of n such that
A21: (decomp b) /. i = <*tb1,tb2*> and
A22: t /. i = (p . tb1) * (r . tb2) by A9, A11, A14;
A23: ( sb1 = tb1 & sb2 = tb2 ) by ;
s /. i = s . i by ;
hence s . i = ((p . sb1) + (q . sb1)) * (r . sb2) by
.= ((p . sb1) * (r . sb2)) + ((q . sb1) * (r . sb2)) by VECTSP_1:def 7
.= (t + u) . i by ;
:: thesis: verum
end;
len (t + u) = len s by ;
then s = t + u by ;
hence ((p + q) *' r) . b = (Sum t) + (Sum u) by
.= ((p *' r) + (q *' r)) . b by ;
:: thesis: verum
end;
hence (p + q) *' r = (p *' r) + (q *' r) by FUNCT_2:63; :: thesis: verum