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;