take len p ; :: according to ALGSEQ_1:def 1 :: 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 12;
assume i >= len p ; :: thesis: (Leading-Monomial p) . i = 0. L
then i + 1 > len p by NAT_1:13;
then A2: (i + 1) - 1 > (len p) - 1 by XREAL_1:9;
A3: Leading-Monomial p = (0_. L) +* (((len p) -' 1),(p . ((len p) -' 1))) by Th11;

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:9;
then i <> (len p) -' 1 by A2, XREAL_0:def 2;
hence (Leading-Monomial p) . i = (0_. L) . i by A3, FUNCT_7:32
.= 0. L by A1, FUNCOP_1:7 ;
:: thesis: verum

end;

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

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

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

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 A3, A5, FUNCT_7:32
.= 0. L by A1, FUNCOP_1:7 ;
:: thesis: verum

end;

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

hence (Leading-Monomial p) . i = p . 0 by A3, A5, A6, FUNCT_7:31
.= (0_. L) . 0 by A4, Th5
.= 0. L by FUNCOP_1:7 ;
:: thesis: verum

end;

end;

end;

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

end;

end;