let n be set ; :: thesis: for L being non empty commutative multLoopStr_0
for p being Series of n,L
for a being Element of L holds a * p = p * a
let L be non empty commutative multLoopStr_0 ; :: thesis: for p being Series of n,L
for a being Element of L holds a * p = p * a
let p be Series of n,L; :: thesis: for a being Element of L holds a * p = p * a
let a be Element of L; :: thesis: a * p = p * a

now

let b be Element of Bags n; :: thesis: (a * p) . b = (p * a) . b
reconsider b' = b as bag of ;
thus (a * p) . b = a * (p . b') by Def10
.= (p * a) . b by Def11 ; :: thesis: verum

end;

hence a * p = p * a by FUNCT_2:113; :: thesis: verum