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 Lm9;
deg (p1 + p2) = deg p2 by A1, POLYNOM3:28
.= 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 Lm9;
deg (p1 + p2) = deg p1 by A3, POLYNOM3:28
.= 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 Lm8;
deg p1 is Element of NAT by A5, Lm8;
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:6;
then A8: p2 . k = 0. L by A7, ALGSEQ_1:8, XXREAL_0:2;
deg p1 <= m by XXREAL_0:25;
then (deg p1) + 1 <= m + 1 by XREAL_1:6;
then p1 . k = 0. L by A7, ALGSEQ_1:8, XXREAL_0:2;
hence (p1 + p2) . k = (0. L) + (0. L) by A8, NORMSP_1:def 2
.= 0. L by RLVECT_1:def 4 ;
:: thesis: verum

end;

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

end;

end;