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:10;

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:11;
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:11;
hence deg (p1 + p2) = max (deg p1),(deg p2) by A1, A3, XXREAL_0:def 10; :: thesis: verum

end;

end;