let n be Ordinal; :: thesis: for L being non empty right_complementable well-unital distributive add-associative right_zeroed associative commutative doubleLoopStr
for p, p9 being Series of n,L
for a being Element of L holds a * (p *' p9) = p *' (a * p9)
let L be non empty right_complementable well-unital distributive add-associative right_zeroed associative commutative doubleLoopStr ; :: thesis: for p, p9 being Series of n,L
for a being Element of L holds a * (p *' p9) = p *' (a * p9)
let p, p9 be Series of n,L; :: thesis: for a being Element of L holds a * (p *' p9) = p *' (a * p9)
let a be Element of L; :: thesis: a * (p *' p9) = p *' (a * p9)
set app = a * (p *' p9);
set pap = p *' (a * p9);
set pp = p *' p9;

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

let u be object ; :: thesis: ( u in dom (a * (p *' p9)) implies (a * (p *' p9)) . u = (p *' (a * p9)) . u )
assume u in dom (a * (p *' p9)) ; :: thesis: (a * (p *' p9)) . u = (p *' (a * p9)) . u
then reconsider b = u as bag of n ;
consider s being FinSequence of the carrier of L such that
A2: (p *' (a * p9)) . b = Sum s and
A3: len s = len (decomp b) and
A4: 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 . b1) * ((a * p9) . b2) ) by POLYNOM1:def 10;
consider t being FinSequence of the carrier of L such that
A5: (p *' p9) . b = Sum t and
A6: len t = len (decomp b) and
A7: 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) * (p9 . b2) ) by POLYNOM1:def 10;
A8: dom t = Seg (len s) by A3, A6, FINSEQ_1:def 3
.= dom s by FINSEQ_1:def 3 ;

now :: thesis: for i being object st i in dom t holds
s /. i = a * (t /. i)

let i be object ; :: thesis: ( i in dom t implies s /. i = a * (t /. i) )
assume A9: i in dom t ; :: thesis: s /. i = a * (t /. i)
then reconsider k = i as Element of NAT ;
consider b1, b2 being bag of n such that
A10: (decomp b) /. k = <*b1,b2*> and
A11: t /. k = (p . b1) * (p9 . b2) by A7, A9;
consider a1, a2 being bag of n such that
A12: (decomp b) /. k = <*a1,a2*> and
A13: s /. k = (p . a1) * ((a * p9) . a2) by A4, A8, A9;
A14: b2 = <*a1,a2*> . 2 by A10, A12
.= a2 ;
b1 = <*a1,a2*> . 1 by A10, A12
.= a1 ;
hence s /. i = (p . b1) * (a * (p9 . b2)) by A13, A14, POLYNOM7:def 9
.= a * (t /. i) by A11, GROUP_1:def 3 ;
:: thesis: verum

end;

then s = a * t by A8, POLYNOM1:def 1;
then (p *' (a * p9)) . b = a * (Sum t) by A2, POLYNOM1:12
.= (a * (p *' p9)) . b by A5, POLYNOM7:def 9 ;
hence (a * (p *' p9)) . u = (p *' (a * p9)) . u ; :: thesis: verum

end;

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