let L be non empty right_complementable Abelian add-associative right_zeroed addLoopStr ; :: thesis: for p1, p2 being Polynomial of L holds deg (p1 + p2) <= max (deg p1),(deg p2)
let p1, p2 be Polynomial of L; :: thesis: deg (p1 + p2) <= max (deg p1),(deg p2)

per cases ( p1 = 0_. L or p2 = 0_. L or ( p1 <> 0_. L & p2 <> 0_. L ) ) ;

suppose A1: p1 = 0_. L ; :: thesis: deg (p1 + p2) <= max (deg p1),(deg p2)

then deg p1 = - 1 by Th20;
then A2: deg p2 >= deg p1 by Lm10;
deg (p1 + p2) = deg p2 by A1, POLYNOM3:29
.= max (deg p1),(deg p2) by A2, XXREAL_0:def 10 ;
hence deg (p1 + p2) <= max (deg p1),(deg p2) ; :: thesis: verum

end;

suppose A3: p2 = 0_. L ; :: thesis: deg (p1 + p2) <= max (deg p1),(deg p2)

then deg p2 = - 1 by Th20;
then A4: deg p1 >= deg p2 by Lm10;
deg (p1 + p2) = deg p1 by A3, POLYNOM3:29
.= max (deg p1),(deg p2) by A4, XXREAL_0:def 10 ;
hence deg (p1 + p2) <= max (deg p1),(deg p2) ; :: thesis: verum

end;

suppose A5: ( p1 <> 0_. L & p2 <> 0_. L ) ; :: thesis: deg (p1 + p2) <= max (deg p1),(deg p2)

then A6: deg p2 is Element of NAT by Lm9;
deg p1 is Element of NAT by A5, Lm9;
then reconsider m = max (deg p1),(deg p2) as Element of NAT by A6, XXREAL_0:16;
for k being Nat st k >= m + 1 holds
(p1 + p2) . k = 0. L

proof

let k be Nat; :: thesis: ( k >= m + 1 implies (p1 + p2) . k = 0. L )
assume A7: k >= m + 1 ; :: thesis: (p1 + p2) . k = 0. L
deg p2 <= m by XXREAL_0:25;
then (deg p2) + 1 <= m + 1 by XREAL_1:8;
then A8: p2 . k = 0. L by A7, ALGSEQ_1:22, XXREAL_0:2;
A9: k in NAT by ORDINAL1:def 13;
deg p1 <= m by XXREAL_0:25;
then (deg p1) + 1 <= m + 1 by XREAL_1:8;
then p1 . k = 0. L by A7, ALGSEQ_1:22, XXREAL_0:2;
hence (p1 + p2) . k = (0. L) + (0. L) by A9, A8, NORMSP_1:def 5
.= 0. L by RLVECT_1:def 7 ;
:: thesis: verum

end;

then m + 1 is_at_least_length_of p1 + p2 by ALGSEQ_1:def 3;
then len (p1 + p2) <= m + 1 by ALGSEQ_1:def 4;
then (len (p1 + p2)) - 1 <= (m + 1) - 1 by XREAL_1:11;
hence deg (p1 + p2) <= max (deg p1),(deg p2) ; :: thesis: verum

end;

end;