let F be Field; :: thesis: 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) ) )
let p, q be Polynomial of F; :: thesis: ( ( 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) ) )

per cases ( ( p <> 0_. F & q <> 0_. F ) or ( p = 0_. F & q <> 0_. F ) or ( q = 0_. F & p <> 0_. F ) or ( q = 0_. F & p = 0_. F ) ) ;

suppose ( p <> 0_. F & q <> 0_. F ) ; :: thesis: ( ( 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) ) )

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

A: now :: thesis: ( deg p > deg q implies LC (p + q) = LC p )

assume A1: deg p > deg q ; :: thesis: LC (p + q) = LC p
then deg p > (len q) - 1 by HURWITZ:def 2;
then deg p >= ((len q) - 1) + 1 by INT_1:7;
then A2: q . (deg p) = 0. F by ALGSEQ_1:8;
A3: (p + q) . (deg p) = (p . (deg p)) + (q . (deg p)) by NORMSP_1:def 2
.= LC p by A2, FIELD_6:2 ;
then p + q <> 0_. F ;
then A4: not p + q is zero by UPROOTS:def 5;
deg (p + q) = deg p by A1, NIVEN:42;
hence LC (p + q) = LC p by A3, A4, FIELD_6:2; :: thesis: verum

end;

B: now :: thesis: ( deg q > deg p implies LC (p + q) = LC q )

assume A1: deg q > deg p ; :: thesis: LC (p + q) = LC q
then deg q > (len p) - 1 by HURWITZ:def 2;
then deg q >= ((len p) - 1) + 1 by INT_1:7;
then A2: p . (deg q) = 0. F by ALGSEQ_1:8;
A3: (p + q) . (deg q) = (p . (deg q)) + (q . (deg q)) by NORMSP_1:def 2
.= LC q by A2, FIELD_6:2 ;
then p + q <> 0_. F ;
then A4: not p + q is zero by UPROOTS:def 5;
deg (p + q) = deg q by A1, NIVEN:42;
hence LC (p + q) = LC q by A3, A4, FIELD_6:2; :: thesis: verum

end;

now :: thesis: ( deg p = deg q & (LC p) + (LC q) <> 0. F implies LC (p + q) = (LC p) + (LC q) )

assume A1: ( deg p = deg q & (LC p) + (LC q) <> 0. F ) ; :: thesis: LC (p + q) = (LC p) + (LC q)
then A2: deg (p + q) = max ((deg p),(deg p)) by lem23a
.= deg p ;
then p + q <> 0_. F by HURWITZ:20;
then not p + q is zero by UPROOTS:def 5;
hence LC (p + q) = (p + q) . (deg q) by A1, A2, FIELD_6:2
.= (p . (deg q)) + (q . (deg q)) by NORMSP_1:def 2
.= (LC p) + (q . (deg q)) by A1, FIELD_6:2
.= (LC p) + (LC q) by FIELD_6:2 ;
:: thesis: verum

end;

hence ( ( 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) ) ) by A, B; :: thesis: verum

end;

suppose A: ( p = 0_. F & q <> 0_. F ) ; :: thesis: ( ( 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) ) )

then reconsider q = q as non zero Polynomial of F by UPROOTS:def 5;
( deg p = - 1 & deg q >= 0 ) by A, HURWITZ:20;
hence ( ( 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) ) ) by A; :: thesis: verum

end;

suppose A: ( q = 0_. F & p <> 0_. F ) ; :: thesis: ( ( 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) ) )

then reconsider p = p as non zero Polynomial of F by UPROOTS:def 5;
( deg q = - 1 & deg p >= 0 ) by A, HURWITZ:20;
hence ( ( 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) ) ) by A; :: thesis: verum

end;

suppose A: ( q = 0_. F & p = 0_. F ) ; :: thesis: ( ( 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) ) )

len (0_. F) = 0 by POLYNOM4:3;
then (len (0_. F)) - 1 < 0 ;
then C: (len (0_. F)) -' 1 = 0 by XREAL_0:def 2;
LC (p + q) = (0_. F) . ((len (0_. F)) -' 1) by A, RATFUNC1:def 6
.= 0. F by C ;
hence ( ( 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) ) ) by A; :: thesis: verum

end;

end;