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

A1: now

let u be set ; :: thesis: ( u in dom ((a * a') * p) implies ((a * a') * p) . u = (a * (a' * p)) . u )
assume u in dom ((a * a') * p) ; :: thesis: ((a * a') * p) . u = (a * (a' * p)) . u
then reconsider b = u as bag of n by PRE_POLY:def 12;
((a * a') * p) . b = (a * a') * (p . b) by POLYNOM7:def 10
.= a * (a' * (p . b)) by GROUP_1:def 4
.= a * ((a' * p) . b) by POLYNOM7:def 10
.= (a * (a' * p)) . b by POLYNOM7:def 10 ;
hence ((a * a') * p) . u = (a * (a' * p)) . u ; :: thesis: verum

end;

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