let L be Field; 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; ( 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
; 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; 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 for i being object st i in dom F1 holds
F2 /. i = (F1 /. i) * ((p . ((len p) -' 1)) ")let i be
object ;
( i in dom F1 implies F2 /. i = (F1 /. i) * ((p . ((len p) -' 1)) ") )assume A9:
i in dom F1
;
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
;
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))
; verum