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, Th41;
hence LC (p - q) = (p . ((len p) -' 1)) - (q . ((len p) -' 1)) by NORMSP_1:def 3
.= LC p by A2
.= 1. L by RATFUNC1:def 7 ;
:: according to RATFUNC1:def 7 :: thesis: verum