let L be Field; :: thesis: for p being Polynomial of L st len p <> 0 holds
len (NormPolynomial p) = len p
let p be Polynomial of L; :: thesis: ( len p <> 0 implies len (NormPolynomial p) = len p )
assume len p <> 0 ; :: thesis: len (NormPolynomial p) = len p
then len p >= 0 + 1 by NAT_1:13;
then len p = ((len p) -' 1) + 1 by XREAL_1:235;
then p . ((len p) -' 1) <> 0. L by ALGSEQ_1:10;
then A1: (p . ((len p) -' 1)) " <> 0. L by VECTSP_1:25;

A2: now :: thesis: for n being Nat st n is_at_least_length_of NormPolynomial p holds
len p <= n

let n be Nat; :: thesis: ( n is_at_least_length_of NormPolynomial p implies len p <= n )
assume A3: n is_at_least_length_of NormPolynomial p ; :: thesis: len p <= n
n is_at_least_length_of p

proof

let i be Nat; :: according to ALGSEQ_1:def 2 :: thesis: ( not n <= i or p . i = 0. L )
reconsider ii = i as Element of NAT by ORDINAL1:def 12;
assume i >= n ; :: thesis: p . i = 0. L
then (NormPolynomial p) . i = 0. L by A3;
then (p . ii) / (p . ((len p) -' 1)) = 0. L by Def11;
then (p . ii) * ((p . ((len p) -' 1)) ") = 0. L ;
hence p . i = 0. L by A1, VECTSP_1:12; :: thesis: verum

end;

hence len p <= n by ALGSEQ_1:def 3; :: thesis: verum

end;

len p is_at_least_length_of NormPolynomial p

proof

let n be Nat; :: according to ALGSEQ_1:def 2 :: thesis: ( not len p <= n or (NormPolynomial p) . n = 0. L )
assume A4: n >= len p ; :: thesis: (NormPolynomial p) . n = 0. L
reconsider nn = n as Element of NAT by ORDINAL1:def 12;
thus (NormPolynomial p) . n = (p . nn) / (p . ((len p) -' 1)) by Def11
.= (0. L) / (p . ((len p) -' 1)) by A4, ALGSEQ_1:8
.= (0. L) * ((p . ((len p) -' 1)) ")
.= 0. L ; :: thesis: verum

end;

hence len (NormPolynomial p) = len p by A2, ALGSEQ_1:def 3; :: thesis: verum