take len p ; :: according to ALGSEQ_1:def 2 :: thesis: for b₁ being set holds
( not len p <= b₁ or (Leading-Monomial p) . b₁ = 0. L )
let i be Nat; :: thesis: ( not len p <= i or (Leading-Monomial p) . i = 0. L )
A1: i in NAT by ORDINAL1:def 13;
A2: Leading-Monomial p = (0_. L) +* ((len p) -' 1),(p . ((len p) -' 1)) by Th14;
assume i >= len p ; :: thesis: (Leading-Monomial p) . i = 0. L
then i + 1 > len p by NAT_1:13;
then A3: (i + 1) - 1 > (len p) - 1 by XREAL_1:11;

per cases ( len p > 0 or len p = 0 ) ;

suppose len p > 0 ; :: thesis: (Leading-Monomial p) . i = 0. L

then len p >= 0 + 1 by NAT_1:13;
then (len p) - 1 >= (0 + 1) - 1 by XREAL_1:11;
then i <> (len p) -' 1 by A3, XREAL_0:def 2;
hence (Leading-Monomial p) . i = (0_. L) . i by A2, FUNCT_7:34
.= 0. L by A1, FUNCOP_1:13 ;
:: thesis: verum

end;

suppose A4: len p = 0 ; :: thesis: (Leading-Monomial p) . i = 0. L

then A5: (len p) -' 1 = 0 by NAT_2:10;
0 in NAT ;
then A6: 0 in dom (0_. L) by NORMSP_1:17;

now

per cases ( i > 0 or i = 0 ) ;

suppose i > 0 ; :: thesis: (Leading-Monomial p) . i = 0. L

hence (Leading-Monomial p) . i = (0_. L) . i by A2, A5, FUNCT_7:34
.= 0. L by A1, FUNCOP_1:13 ;
:: thesis: verum

end;

suppose i = 0 ; :: thesis: (Leading-Monomial p) . i = 0. L

hence (Leading-Monomial p) . i = p . 0 by A2, A5, A6, FUNCT_7:33
.= (0_. L) . 0 by A4, Th8
.= 0. L by FUNCOP_1:13 ;
:: thesis: verum

end;

end;

end;

hence (Leading-Monomial p) . i = 0. L ; :: thesis: verum

end;

end;