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 :: thesis: for b being Element of Bags n holds (a * p) . b = (p * a) . b
let b be Element of Bags n; :: thesis: (a * p) . b = (p * a) . b
reconsider b9 = b as bag of n ;
thus (a * p) . b = a * (p . b9) by Def9
.= (p * a) . b by Def10 ; :: thesis: verum
end;
hence a * p = p * a ; :: thesis: verum