theorem Th7: :: POLYNOM4:7

for L being non empty right_complementable add-associative right_zeroed addLoopStr
for p, q being Polynomial of L st len p <> len q holds
len (p + q) = max ((len p),(len q))