theorem :: POLYNOM3:24

for L being non empty right_zeroed addLoopStr
for p, q being Polynomial of L
for n being Element of NAT st n is_at_least_length_of p & n is_at_least_length_of q holds
n is_at_least_length_of p + q