let L be non empty right_complementable add-associative right_zeroed addLoopStr ; :: thesis: for p being Polynomial of L holds (p || ((len p) -' 1)) + (Leading-Monomial p) = p
let p be Polynomial of L; :: thesis: (p || ((len p) -' 1)) + (Leading-Monomial p) = p
set l = Leading-Monomial p;
set m = (len p) -' 1;
let n be Element of NAT ; :: according to FUNCT_2:def 8 :: thesis: ((p || ((len p) -' 1)) + (Leading-Monomial p)) . n = p . n
A1: ((p || ((len p) -' 1)) + (Leading-Monomial p)) . n = ((p || ((len p) -' 1)) . n) + ((Leading-Monomial p) . n) by NORMSP_1:def 2;

per cases ( n = (len p) -' 1 or n <> (len p) -' 1 ) ;

suppose A2: n = (len p) -' 1 ; :: thesis: ((p || ((len p) -' 1)) + (Leading-Monomial p)) . n = p . n

(p || ((len p) -' 1)) . ((len p) -' 1) = 0. L by Th32;
hence ((p || ((len p) -' 1)) + (Leading-Monomial p)) . n = p . n by A1, A2, POLYNOM4:def 1; :: thesis: verum

end;

suppose A3: n <> (len p) -' 1 ; :: thesis: ((p || ((len p) -' 1)) + (Leading-Monomial p)) . n = p . n

then (Leading-Monomial p) . n = 0. L by POLYNOM4:def 1;
hence ((p || ((len p) -' 1)) + (Leading-Monomial p)) . n = p . n by A1, A3, FUNCT_7:32; :: thesis: verum

end;

end;