for L being non empty right_complementable add-associative right_zeroed well-unital distributive doubleLoopStr
for p, q being Polynomial of L holds len (p *' q) <= ((len p) + (len q)) -' 1