let L be non empty ZeroStr ; :: thesis: for p being Polynomial of L holds Leading-Monomial p = (0_. L) +* (((len p) -' 1),(p . ((len p) -' 1)))
let p be Polynomial of L; :: thesis: Leading-Monomial p = (0_. L) +* (((len p) -' 1),(p . ((len p) -' 1)))
reconsider P = (0_. L) +* (((len p) -' 1),(p . ((len p) -' 1))) as sequence of L ;

A1: now :: thesis: for n being Element of NAT st n <> (len p) -' 1 holds
P . n = 0. L

let n be Element of NAT ; :: thesis: ( n <> (len p) -' 1 implies P . n = 0. L )
assume n <> (len p) -' 1 ; :: thesis: P . n = 0. L
hence P . n = (0_. L) . n by FUNCT_7:32
.= 0. L by FUNCOP_1:7 ;
:: thesis: verum

end;

(len p) -' 1 in NAT ;
then (len p) -' 1 in dom (0_. L) by NORMSP_1:12;
then P . ((len p) -' 1) = p . ((len p) -' 1) by FUNCT_7:31;
hence Leading-Monomial p = (0_. L) +* (((len p) -' 1),(p . ((len p) -' 1))) by A1, Def1; :: thesis: verum