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

now

let u be set ; :: thesis: ( u in dom (a * (p *' p')) implies (a * (p *' p')) . u = (p *' (a * p')) . u )
assume u in dom (a * (p *' p')) ; :: thesis: (a * (p *' p')) . u = (p *' (a * p')) . u
then reconsider b = u as bag of by POLYNOM1:def 14;
consider s being FinSequence of the carrier of L such that
A2: ( (p *' (a * p')) . b = Sum s & len s = len (decomp b) & ( for k being Element of NAT st k in dom s holds
ex b1, b2 being bag of st
( (decomp b) /. k = <*b1,b2*> & s /. k = (p . b1) * ((a * p') . b2) ) ) ) by POLYNOM1:def 26;
consider t being FinSequence of the carrier of L such that
A3: ( (p *' p') . b = Sum t & len t = len (decomp b) & ( for k being Element of NAT st k in dom t holds
ex b1, b2 being bag of st
( (decomp b) /. k = <*b1,b2*> & t /. k = (p . b1) * (p' . b2) ) ) ) by POLYNOM1:def 26;
A4: dom t = Seg (len s) by A2, A3, FINSEQ_1:def 3
.= dom s by FINSEQ_1:def 3 ;

now

let i be set ; :: thesis: ( i in dom t implies s /. i = a * (t /. i) )
assume A5: i in dom t ; :: thesis: s /. i = a * (t /. i)
then reconsider k = i as Element of NAT ;
consider b1, b2 being bag of such that
A6: ( (decomp b) /. k = <*b1,b2*> & t /. k = (p . b1) * (p' . b2) ) by A3, A5;
consider a1, a2 being bag of such that
A7: ( (decomp b) /. k = <*a1,a2*> & s /. k = (p . a1) * ((a * p') . a2) ) by A2, A4, A5;
A8: b1 = <*a1,a2*> . 1 by A6, A7, FINSEQ_1:61
.= a1 by FINSEQ_1:61 ;
b2 = <*a1,a2*> . 2 by A6, A7, FINSEQ_1:61
.= a2 by FINSEQ_1:61 ;
hence s /. i = (p . b1) * (a * (p' . b2)) by A7, A8, POLYNOM7:def 10
.= a * (t /. i) by A6, GROUP_1:def 4 ;
:: thesis: verum

end;

then s = a * t by A4, POLYNOM1:def 2;
then (p *' (a * p')) . b = a * (Sum t) by A2, POLYNOM1:28
.= (a * (p *' p')) . b by A3, POLYNOM7:def 10 ;
hence (a * (p *' p')) . u = (p *' (a * p')) . u ; :: thesis: verum

end;

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