let F be Field; :: thesis: for p, q being Polynomial of F st (LC p) + (LC q) <> 0. F holds
deg (p + q) = max ((deg p),(deg q))
let p1, q1 be Polynomial of F; :: thesis: ( (LC p1) + (LC q1) <> 0. F implies deg (p1 + q1) = max ((deg p1),(deg q1)) )
assume AS: (LC p1) + (LC q1) <> 0. F ; :: thesis: deg (p1 + q1) = max ((deg p1),(deg q1))

per cases ( ( p1 <> 0_. F & q1 <> 0_. F ) or p1 = 0_. F or q1 = 0_. F ) ;

suppose ( p1 <> 0_. F & q1 <> 0_. F ) ; :: thesis: deg (p1 + q1) = max ((deg p1),(deg q1))

then reconsider p = p1, q = q1 as non zero Polynomial of F by UPROOTS:def 5;

per cases ( deg p = deg q or deg p <> deg q ) ;

suppose A: deg p = deg q ; :: thesis: deg (p1 + q1) = max ((deg p1),(deg q1))

(p + q) . (deg p) = (p . (deg p)) + (q . (deg p)) by NORMSP_1:def 2
.= (LC p) + (q . (deg q)) by A, FIELD_6:2
.= (LC p) + (LC q) by FIELD_6:2 ;
then len (p + q) >= (deg p) + 1 by AS, ALGSEQ_1:8, INT_1:7;
then (len (p + q)) - 1 >= ((deg p) + 1) - 1 by XREAL_1:9;
then B: deg (p + q) >= deg p by HURWITZ:def 2;
deg (p + q) <= max ((deg p),(deg q)) by HURWITZ:22;
hence deg (p1 + q1) = max ((deg p1),(deg q1)) by A, B, XXREAL_0:1; :: thesis: verum

end;

suppose deg p <> deg q ; :: thesis: deg (p1 + q1) = max ((deg p1),(deg q1))

hence deg (p1 + q1) = max ((deg p1),(deg q1)) by HURWITZ:21; :: thesis: verum

end;

end;

end;

suppose A: p1 = 0_. F ; :: thesis: deg (p1 + q1) = max ((deg p1),(deg q1))

then C: deg p1 = - 1 by HURWITZ:20;
(len q1) - 1 >= 0 - 1 by XREAL_1:9;
then deg q1 >= deg p1 by C, HURWITZ:def 2;
hence deg (p1 + q1) = max ((deg p1),(deg q1)) by A, XXREAL_0:def 10; :: thesis: verum

end;

suppose A: q1 = 0_. F ; :: thesis: deg (p1 + q1) = max ((deg p1),(deg q1))

then C: deg q1 = - 1 by HURWITZ:20;
(len p1) - 1 >= 0 - 1 by XREAL_1:9;
then deg p1 >= deg q1 by C, HURWITZ:def 2;
hence deg (p1 + q1) = max ((deg p1),(deg q1)) by A, XXREAL_0:def 10; :: thesis: verum

end;

end;