let L be non empty right_complementable add-associative right_zeroed addLoopStr ; :: thesis: for p1, p2 being Polynomial of L st deg p1 <> deg p2 holds
deg (p1 + p2) = max ((deg p1),(deg p2))
let p1, p2 be Polynomial of L; :: thesis: ( deg p1 <> deg p2 implies deg (p1 + p2) = max ((deg p1),(deg p2)) )
assume deg p1 <> deg p2 ; :: thesis: deg (p1 + p2) = max ((deg p1),(deg p2))
then A1: deg (p1 + p2) = (max ((len p1),(len p2))) - 1 by POLYNOM4:7;

per cases ( max ((len p1),(len p2)) = len p1 or max ((len p1),(len p2)) = len p2 ) by XXREAL_0:16;

suppose A2: max ((len p1),(len p2)) = len p1 ; :: thesis: deg (p1 + p2) = max ((deg p1),(deg p2))

then len p2 <= len p1 by XXREAL_0:25;
then deg p2 <= deg p1 by XREAL_1:9;
hence deg (p1 + p2) = max ((deg p1),(deg p2)) by A1, A2, XXREAL_0:def 10; :: thesis: verum

end;

suppose A3: max ((len p1),(len p2)) = len p2 ; :: thesis: deg (p1 + p2) = max ((deg p1),(deg p2))

then len p1 <= len p2 by XXREAL_0:25;
then deg p1 <= deg p2 by XREAL_1:9;
hence deg (p1 + p2) = max ((deg p1),(deg p2)) by A1, A3, XXREAL_0:def 10; :: thesis: verum

end;

end;