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

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:34
.= 0. L by FUNCOP_1:13 ;
:: thesis: verum

end;

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