let L be non degenerated right_complementable add-associative right_zeroed distributive doubleLoopStr ; :: thesis: for p being monic Polynomial of L
for q being Polynomial of L st deg p > deg q holds
p + q is monic
let p be monic Polynomial of L; :: thesis: for q being Polynomial of L st deg p > deg q holds
p + q is monic
let q be Polynomial of L; :: thesis: ( deg p > deg q implies p + q is monic )
assume A1: deg p > deg q ; :: thesis: p + q is monic
then A2: q . ((len p) -' 1) = 0. L by Lm3;
deg (p + q) = deg p by A1, Th40;
hence LC (p + q) = (p . ((len p) -' 1)) + (q . ((len p) -' 1)) by NORMSP_1:def 2
.= LC p by A2
.= 1. L by RATFUNC1:def 7 ;
:: according to RATFUNC1:def 7 :: thesis: verum