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 ;
then len p >= 0 + 1 by NAT_1:13;
then len p = ((len p) -' 1) + 1 by XREAL_1:237;
then p . ((len p) -' 1) <> 0. L by ALGSEQ_1:25;
then A1: (p . ((len p) -' 1)) " <> 0. L by VECTSP_1:74;
A2: len p is_at_least_length_of NormPolynomial p

proof

let n be Nat; :: according to ALGSEQ_1:def 3 :: thesis: ( not len p <= n or (NormPolynomial p) . n = 0. L )
assume A3: n >= len p ; :: thesis: (NormPolynomial p) . n = 0. L
reconsider nn = n as Element of NAT by ORDINAL1:def 13;
thus (NormPolynomial p) . n = (p . nn) / (p . ((len p) -' 1)) by Def10
.= (0. L) / (p . ((len p) -' 1)) by A3, ALGSEQ_1:22
.= (0. L) * ((p . ((len p) -' 1)) " ) by VECTSP_1:def 23
.= 0. L by VECTSP_1:39 ; :: thesis: verum

end;

now

let n be Nat; :: thesis: ( n is_at_least_length_of NormPolynomial p implies len p <= n )
assume A4: 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 3 :: thesis: ( not n <= i or p . i = 0. L )
assume Z: i >= n ; :: thesis: p . i = 0. L
reconsider ii = i as Element of NAT by ORDINAL1:def 13;
(NormPolynomial p) . i = 0. L by A4, Z, ALGSEQ_1:def 3;
then (p . ii) / (p . ((len p) -' 1)) = 0. L by Def10;
then (p . ii) * ((p . ((len p) -' 1)) " ) = 0. L by VECTSP_1:def 23;
hence p . i = 0. L by A1, VECTSP_1:44; :: thesis: verum

end;

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

end;

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