let L be non empty associative doubleLoopStr ; :: thesis: for k, l being Element of L
for seq being sequence of L holds k * (l * seq) = (k * l) * seq
let k, l be Element of L; :: thesis: for seq being sequence of L holds k * (l * seq) = (k * l) * seq
let seq be sequence of L; :: thesis: k * (l * seq) = (k * l) * seq

now :: thesis: for i being Element of NAT holds (k * (l * seq)) . i = ((k * l) * seq) . i

let i be Element of NAT ; :: thesis: (k * (l * seq)) . i = ((k * l) * seq) . i
thus (k * (l * seq)) . i = k * ((l * seq) . i) by POLYNOM5:def 4
.= k * (l * (seq . i)) by POLYNOM5:def 4
.= (k * l) * (seq . i) by GROUP_1:def 3
.= ((k * l) * seq) . i by POLYNOM5:def 4 ; :: thesis: verum

end;

hence k * (l * seq) = (k * l) * seq by FUNCT_2:63; :: thesis: verum