let L be non empty right_complementable add-associative right_zeroed addLoopStr ; :: thesis: for p, q being Polynomial of L st deg p > deg q holds
deg (p + q) = deg p
let p, q be Polynomial of L; :: thesis: ( deg p > deg q implies deg (p + q) = deg p )
assume A1: deg p > deg q ; :: thesis: deg (p + q) = deg p
then deg (p + q) = max ((deg p),(deg q)) by HURWITZ:21;
hence deg (p + q) = deg p by A1, XXREAL_0:def 10; :: thesis: verum