let L be non empty non degenerated multLoopStr_0 ; :: thesis: Leading-Monomial (1_. L) = 1_. L

A1: now :: thesis: for n being Element of NAT st n <> (len (1_. L)) -' 1 holds
(1_. L) . n = 0. L

let n be Element of NAT ; :: thesis: ( n <> (len (1_. L)) -' 1 implies (1_. L) . n = 0. L )
assume n <> (len (1_. L)) -' 1 ; :: thesis: (1_. L) . n = 0. L
then n <> 1 -' 1 by Th4;
then n <> 0 by XREAL_1:232;
hence (1_. L) . n = 0. L by POLYNOM3:30; :: thesis: verum

end;

(1_. L) . ((len (1_. L)) -' 1) = (1_. L) . ((len (1_. L)) -' 1) ;
hence Leading-Monomial (1_. L) = 1_. L by A1, Def1; :: thesis: verum