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

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

hence
k * (l * seq) = (k * l) * seq
by FUNCT_2:63; :: thesis: verumlet 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;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