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

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

hence
a * p = p * a
; :: thesis: verumlet 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;reconsider b9 = b as bag of n ;

thus (a * p) . b = a * (p . b9) by Def9

.= (p * a) . b by Def10 ; :: thesis: verum