theorem Th6: :: POLYNOM4:6

for L being non empty right_zeroed addLoopStr
for p, q being Polynomial of L
for n being Element of NAT st n >= len p & n >= len q holds
n >= len (p + q)