let L be Field; :: thesis: for p being Polynomial of L st len p <> 0 holds
for x being Element of L holds eval ((NormPolynomial p),x) = (eval (p,x)) / (p . ((len p) -' 1))
let p be Polynomial of L; :: thesis: ( len p <> 0 implies for x being Element of L holds eval ((NormPolynomial p),x) = (eval (p,x)) / (p . ((len p) -' 1)) )
assume A1: len p <> 0 ; :: thesis: for x being Element of L holds eval ((NormPolynomial p),x) = (eval (p,x)) / (p . ((len p) -' 1))
set NPp = NormPolynomial p;
let x be Element of L; :: thesis: eval ((NormPolynomial p),x) = (eval (p,x)) / (p . ((len p) -' 1))
consider F1 being FinSequence of the carrier of L such that
A2: eval (p,x) = Sum F1 and
A3: len F1 = len p and
A4: for n being Element of NAT st n in dom F1 holds
F1 . n = (p . (n -' 1)) * ((power L) . (x,(n -' 1))) by POLYNOM4:def 2;
consider F2 being FinSequence of the carrier of L such that
A5: eval ((NormPolynomial p),x) = Sum F2 and
A6: len F2 = len (NormPolynomial p) and
A7: for n being Element of NAT st n in dom F2 holds
F2 . n = ((NormPolynomial p) . (n -' 1)) * ((power L) . (x,(n -' 1))) by POLYNOM4:def 2;
len F1 = len F2 by A1, A3, A6, Th57;
then A8: dom F1 = dom F2 by FINSEQ_3:29;

now :: thesis: for i being object st i in dom F1 holds
F2 /. i = (F1 /. i) * ((p . ((len p) -' 1)) ")

let i be object ; :: thesis: ( i in dom F1 implies F2 /. i = (F1 /. i) * ((p . ((len p) -' 1)) ") )
assume A9: i in dom F1 ; :: thesis: F2 /. i = (F1 /. i) * ((p . ((len p) -' 1)) ")
then reconsider i1 = i as Element of NAT ;
A10: (p . (i1 -' 1)) * ((power L) . (x,(i1 -' 1))) = F1 . i by A4, A9
.= F1 /. i by A9, PARTFUN1:def 6 ;
thus F2 /. i = F2 . i by A8, A9, PARTFUN1:def 6
.= ((NormPolynomial p) . (i1 -' 1)) * ((power L) . (x,(i1 -' 1))) by A7, A8, A9
.= ((p . (i1 -' 1)) / (p . ((len p) -' 1))) * ((power L) . (x,(i1 -' 1))) by Def11
.= ((p . (i1 -' 1)) * ((p . ((len p) -' 1)) ")) * ((power L) . (x,(i1 -' 1)))
.= (F1 /. i) * ((p . ((len p) -' 1)) ") by A10, GROUP_1:def 3 ; :: thesis: verum

end;

then F2 = F1 * ((p . ((len p) -' 1)) ") by A8, POLYNOM1:def 2;
then eval ((NormPolynomial p),x) = (eval (p,x)) * ((p . ((len p) -' 1)) ") by A2, A5, POLYNOM1:13;
hence eval ((NormPolynomial p),x) = (eval (p,x)) / (p . ((len p) -' 1)) ; :: thesis: verum