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 (decomp b) and
A3: for k being Element of NAT st k in dom s holds
ex b1, b2 being bag of n st
( (decomp b) /. 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 (decomp b) and
A6: for k being Element of NAT st k in dom u holds
ex b1, b2 being bag of n st
( (decomp b) /. 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 (decomp b) and
A9: for k being Element of NAT st k in dom t holds
ex b1, b2 being bag of n st
( (decomp b) /. 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 A2, A8, A5, FINSEQ_2:92;
A10: dom u = dom s by A2, A5, FINSEQ_3:29;
A11: dom t = dom s by A2, A8, FINSEQ_3:29;
then A12: dom (t + u) = dom s by A10, POLYNOM1:1;

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 A11, A10, A14, PARTFUN1:def 6;
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 A15, A18, FINSEQ_1:77;
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 A15, A21, FINSEQ_1:77;
s /. i = s . i by A14, PARTFUN1:def 6;
hence s . i = ((p . sb1) + (q . sb1)) * (r . sb2) by A16, POLYNOM1:15
.= ((p . sb1) * (r . sb2)) + ((q . sb1) * (r . sb2)) by VECTSP_1:def 7
.= (t + u) . i by A12, A14, A22, A19, A23, A20, A17, FVSUM_1:17 ;
:: thesis: verum

end;

len (t + u) = len s by A12, FINSEQ_3:29;
then s = t + u by A13, FINSEQ_2:9;
hence ((p + q) *' r) . b = (Sum t) + (Sum u) by A1, FVSUM_1:76
.= ((p *' r) + (q *' r)) . b by A7, A4, POLYNOM1:15 ;
:: thesis: verum

end;

hence (p + q) *' r = (p *' r) + (q *' r) by FUNCT_2:63; :: thesis: verum