theorem :: POLYNOM4:10

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