theorem lem23a: :: REALALG3:9

for F being Field
for p, q being Polynomial of F st (LC p) + (LC q) <> 0. F holds
deg (p + q) = max ((deg p),(deg q))