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 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 holds a * (p *' p') = p *' (a * p')
let p, p' be Series of n,L; :: thesis: for a being Element of holds a * (p *' p') = p *' (a * p')
let a be Element of ; :: thesis: a * (p *' p') = p *' (a * p')
set app = a * (p *' p');
set pap = p *' (a * p');
set pp = p *' p';

A1: 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 n by PRE_POLY:def 12;
consider s being FinSequence of the carrier of L such that
A2: (p *' (a * p')) . 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 * p') . b2) ) by POLYNOM1:def 26;
consider t being FinSequence of the carrier of L such that
A5: (p *' p') . 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) * (p' . b2) ) by POLYNOM1:def 26;
A8: dom t = Seg (len s) by A3, A6, 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 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) * (p' . 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 * p') . a2) by A4, A8, A9;
A14: b2 = <*a1,a2*> . 2 by A10, A12, FINSEQ_1:61
.= a2 by FINSEQ_1:61 ;
b1 = <*a1,a2*> . 1 by A10, A12, FINSEQ_1:61
.= a1 by FINSEQ_1:61 ;
hence s /. i = (p . b1) * (a * (p' . b2)) by A13, A14, POLYNOM7:def 10
.= a * (t /. i) by A11, GROUP_1:def 4 ;
:: thesis: verum

end;

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

end;

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