for L being non empty right_complementable well-unital distributive add-associative right_zeroed associative commutative doubleLoopStr
for p, q being Polynomial of L st (p . ((len p) -' 1)) * (q . ((len q) -' 1)) <> 0. L holds
0 < len (p *' q)