let F be Field; :: thesis: for E being FieldExtension of F
for p being Element of the carrier of (Polynom-Ring F)
for q being Element of the carrier of (Polynom-Ring E) st p = q holds
NormPolynomial p = NormPolynomial q
let E be FieldExtension of F; :: thesis: for p being Element of the carrier of (Polynom-Ring F)
for q being Element of the carrier of (Polynom-Ring E) st p = q holds
NormPolynomial p = NormPolynomial q
let p be Element of the carrier of (Polynom-Ring F); :: thesis: for q being Element of the carrier of (Polynom-Ring E) st p = q holds
NormPolynomial p = NormPolynomial q
let q be Element of the carrier of (Polynom-Ring E); :: thesis: ( p = q implies NormPolynomial p = NormPolynomial q )
assume AS: p = q ; :: thesis: NormPolynomial p = NormPolynomial q
set np = NormPolynomial p;
set nq = NormPolynomial q;
B1: F is Subfield of E by FIELD_4:7;
B: F is Subring of E by FIELD_4:def 1;

per cases ( q is zero or not q is zero ) ;

suppose q is zero ; :: thesis: NormPolynomial p = NormPolynomial q

then B: q = 0_. E by UPROOTS:def 5;
then A: NormPolynomial q = 0_. E by RING_4:22
.= 0_. F by FIELD_4:12 ;
p = 0_. F by AS, B, FIELD_4:12;
hence NormPolynomial p = NormPolynomial q by A, RING_4:22; :: thesis: verum

end;

suppose not q is zero ; :: thesis: NormPolynomial p = NormPolynomial q

then not LC q is zero ;
then A1: not q . ((len q) -' 1) is zero by RATFUNC1:def 6;
(len p) - 1 = deg p by HURWITZ:def 2
.= deg q by AS, FIELD_4:20
.= (len q) - 1 by HURWITZ:def 2 ;
then A: (p . ((len p) -' 1)) " = (q . ((len q) -' 1)) " by AS, A1, B1, Th19f;

now :: thesis: for n being Element of NAT holds (NormPolynomial p) . n = (NormPolynomial q) . n

let n be Element of NAT ; :: thesis: (NormPolynomial p) . n = (NormPolynomial q) . n
thus (NormPolynomial p) . n = (p . n) / (p . ((len p) -' 1)) by POLYNOM5:def 11
.= (q . n) / (q . ((len q) -' 1)) by B, A, AS, Th18
.= (NormPolynomial q) . n by POLYNOM5:def 11 ; :: thesis: verum

end;

hence NormPolynomial p = NormPolynomial q ; :: thesis: verum

end;

end;