let n be Ordinal; :: thesis: for L being non empty right_add-cancelable right-distributive left_zeroed doubleLoopStr
for p being Series of n,L
for b being bag of
for a being Element of L holds b *' (a * p) = a * (b *' p)
let L be non empty right_add-cancelable right-distributive left_zeroed doubleLoopStr ; :: thesis: for p being Series of n,L
for b being bag of
for a being Element of L holds b *' (a * p) = a * (b *' p)
let p be Series of n,L; :: thesis: for b being bag of
for a being Element of L holds b *' (a * p) = a * (b *' p)
let b be bag of ; :: thesis: for a being Element of L holds b *' (a * p) = a * (b *' p)
let a be Element of L; :: thesis: b *' (a * p) = a * (b *' p)
set q1 = b *' (a * p);
set q2 = a * (b *' p);
A1: dom (b *' (a * p)) = Bags n by FUNCT_2:def 1
.= dom (a * (b *' p)) by FUNCT_2:def 1 ;

now

let x be set ; :: thesis: ( x in dom (b *' (a * p)) implies (b *' (a * p)) . x = (a * (b *' p)) . x )
assume x in dom (b *' (a * p)) ; :: thesis: (b *' (a * p)) . x = (a * (b *' p)) . x
then reconsider u = x as bag of by POLYNOM1:def 14;

now

per cases ( b divides u or not b divides u ) ;

case A2: b divides u ; :: thesis: (b *' (a * p)) . u = (a * (b *' p)) . u

hence (b *' (a * p)) . u = (a * p) . (u -' b) by POLYRED:def 1
.= a * (p . (u -' b)) by POLYNOM7:def 10
.= a * ((b *' p) . u) by A2, POLYRED:def 1
.= (a * (b *' p)) . u by POLYNOM7:def 10 ;
:: thesis: verum

end;

case A3: not b divides u ; :: thesis: (b *' (a * p)) . u = (a * (b *' p)) . u

hence (b *' (a * p)) . u = 0. L by POLYRED:def 1
.= a * (0. L) by BINOM:2
.= a * ((b *' p) . u) by A3, POLYRED:def 1
.= (a * (b *' p)) . u by POLYNOM7:def 10 ;
:: thesis: verum

end;

end;

end;

hence (b *' (a * p)) . x = (a * (b *' p)) . x ; :: thesis: verum

end;

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