for L being non empty right_complementable distributive add-associative right_zeroed domRing-like doubleLoopStr
for m1, m2 being AlgSequence of L st len m1 = len m2 holds
len (m1 * m2) = len m1