theorem lem23d: :: REALALG3:10

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