let L be non empty ZeroStr ; :: thesis: for p being Polynomial of L st len p = 0 holds
Leading-Monomial p = 0_. L
let p be Polynomial of L; :: thesis: ( len p = 0 implies Leading-Monomial p = 0_. L )
assume len p = 0 ; :: thesis: Leading-Monomial p = 0_. L
then A1: (0_. L) . ((len p) -' 1) = p . ((len p) -' 1) by Th5;
for n being Element of NAT st n <> (len p) -' 1 holds
(0_. L) . n = 0. L by FUNCOP_1:7;
hence Leading-Monomial p = 0_. L by A1, Def1; :: thesis: verum