for L being non empty associative doubleLoopStr
for k, l being Element of L
for seq being sequence of L holds k * (l * seq) = (k * l) * seq