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;

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

hence
(p + q) *' r = (p *' r) + (q *' r)
by FUNCT_2:63; :: thesis: verumlet 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;

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;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

len (t + u) = len s
by A12, FINSEQ_3:29;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;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

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