let L be non empty associative doubleLoopStr ; :: thesis: for p being Polynomial of L
for x1, x2 being Element of L holds x1 * (x2 * p) = (x1 * x2) * p
let p be Polynomial of L; :: thesis: for x1, x2 being Element of L holds x1 * (x2 * p) = (x1 * x2) * p
let x1, x2 be Element of L; :: thesis: x1 * (x2 * p) = (x1 * x2) * p
set f = x1 * (x2 * p);
set g = (x1 * x2) * p;

A1: now :: thesis: for i9 being object st i9 in dom (x1 * (x2 * p)) holds
(x1 * (x2 * p)) . i9 = ((x1 * x2) * p) . i9

let i9 be object ; :: thesis: ( i9 in dom (x1 * (x2 * p)) implies (x1 * (x2 * p)) . i9 = ((x1 * x2) * p) . i9 )
assume i9 in dom (x1 * (x2 * p)) ; :: thesis: (x1 * (x2 * p)) . i9 = ((x1 * x2) * p) . i9
then reconsider i = i9 as Element of NAT ;
(x1 * (x2 * p)) . i = x1 * ((x2 * p) . i) by POLYNOM5:def 4
.= x1 * (x2 * (p . i)) by POLYNOM5:def 4
.= (x1 * x2) * (p . i) by GROUP_1:def 3
.= ((x1 * x2) * p) . i by POLYNOM5:def 4 ;
hence (x1 * (x2 * p)) . i9 = ((x1 * x2) * p) . i9 ; :: thesis: verum

end;

dom (x1 * (x2 * p)) = NAT by FUNCT_2:def 1
.= dom ((x1 * x2) * p) by FUNCT_2:def 1 ;
hence x1 * (x2 * p) = (x1 * x2) * p by A1, FUNCT_1:2; :: thesis: verum