let L be non empty ZeroStr ; :: thesis: for p being Polynomial of L holds len (Leading-Monomial p) = len p
let p be Polynomial of L; :: thesis: len (Leading-Monomial p) = len p
set r = Leading-Monomial p;
A1: 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: len (Leading-Monomial p) = len p

then A2: len p >= 0 + 1 by NAT_1:13;
(len p) -' 1 in NAT ;
then A3: (len p) -' 1 in dom (0_. L) by NORMSP_1:12;

A4: now :: thesis: for m being Nat st m is_at_least_length_of Leading-Monomial p holds
not len p > m

let m be Nat; :: thesis: ( m is_at_least_length_of Leading-Monomial p implies not len p > m )
assume A5: m is_at_least_length_of Leading-Monomial p ; :: thesis: not len p > m
assume len p > m ; :: thesis: contradiction
then len p >= m + 1 by NAT_1:13;
then (len p) - 1 >= (m + 1) - 1 by XREAL_1:9;
then (len p) -' 1 >= m by XREAL_0:def 2;
then (Leading-Monomial p) . ((len p) -' 1) = 0. L by A5;
then A6: p . ((len p) -' 1) = 0. L by A1, A3, FUNCT_7:31;
len p = ((len p) -' 1) + 1 by A2, XREAL_1:235;
hence contradiction by A6, ALGSEQ_1:10; :: thesis: verum

end;

A7: (len p) - 1 >= 0 by A2, XREAL_1:19;
len p is_at_least_length_of Leading-Monomial p

proof

let i be Nat; :: according to ALGSEQ_1:def 2 :: thesis: ( not len p <= i or (Leading-Monomial p) . i = 0. L )
A8: 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 (i + 1) - 1 > (len p) - 1 by XREAL_1:9;
then i <> (len p) -' 1 by A7, XREAL_0:def 2;
hence (Leading-Monomial p) . i = (0_. L) . i by A1, FUNCT_7:32
.= 0. L by A8, FUNCOP_1:7 ;
:: thesis: verum

end;

hence len (Leading-Monomial p) = len p by A4, ALGSEQ_1:def 3; :: thesis: verum

end;

suppose A9: len p = 0 ; :: thesis: len (Leading-Monomial p) = len p

hence len (Leading-Monomial p) = len (0_. L) by Th12
.= len p by A9, Th5 ;
:: thesis: verum

end;

end;