let L be non empty associative multMagma ; :: thesis: for p being sequence of L
for a, b being Element of L holds (a * b) * p = a * (b * p)
let p be sequence of L; :: thesis: for a, b being Element of L holds (a * b) * p = a * (b * p)
let a, b be Element of L; :: thesis: (a * b) * p = a * (b * p)

now :: thesis: for x being object st x in NAT holds
((a * b) * p) . x = (a * (b * p)) . x

let x be object ; :: thesis: ( x in NAT implies ((a * b) * p) . x = (a * (b * p)) . x )
assume x in NAT ; :: thesis: ((a * b) * p) . x = (a * (b * p)) . x
then reconsider i = x as Element of NAT ;
thus ((a * b) * p) . x = (a * b) * (p . i) by POLYNOM5:def 4
.= a * (b * (p . i)) by GROUP_1:def 3
.= a * ((b * p) . i) by POLYNOM5:def 4
.= (a * (b * p)) . x by POLYNOM5:def 4 ; :: thesis: verum

end;

hence (a * b) * p = a * (b * p) by FUNCT_2:12; :: thesis: verum