let n be set ; :: thesis: for L being non empty associative multLoopStr_0
for p being Series of n,L
for a, a9 being Element of L holds (a * a9) * p = a * (a9 * p)
let L be non empty associative multLoopStr_0 ; :: thesis: for p being Series of n,L
for a, a9 being Element of L holds (a * a9) * p = a * (a9 * p)
let p be Series of n,L; :: thesis: for a, a9 being Element of L holds (a * a9) * p = a * (a9 * p)
let a, a9 be Element of L; :: thesis: (a * a9) * p = a * (a9 * p)
set q = (a * a9) * p;
set r = a * (a9 * p);

A1: now :: thesis: for u being object st u in dom ((a * a9) * p) holds
((a * a9) * p) . u = (a * (a9 * p)) . u

let u be object ; :: thesis: ( u in dom ((a * a9) * p) implies ((a * a9) * p) . u = (a * (a9 * p)) . u )
assume u in dom ((a * a9) * p) ; :: thesis: ((a * a9) * p) . u = (a * (a9 * p)) . u
then reconsider b = u as bag of n ;
((a * a9) * p) . b = (a * a9) * (p . b) by POLYNOM7:def 9
.= a * (a9 * (p . b)) by GROUP_1:def 3
.= a * ((a9 * p) . b) by POLYNOM7:def 9
.= (a * (a9 * p)) . b by POLYNOM7:def 9 ;
hence ((a * a9) * p) . u = (a * (a9 * p)) . u ; :: thesis: verum

end;

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