theorem Th11: :: POLYNOM8:11

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