let F1 be Field; :: thesis: for F2 being F1 -homomorphic F1 -monomorphic Field
for h being Monomorphism of F1,F2
for p being Element of the carrier of (Polynom-Ring F1) holds NormPolynomial ((PolyHom h) . p) = (PolyHom h) . (NormPolynomial p)
let F2 be F1 -homomorphic F1 -monomorphic Field; :: thesis: for h being Monomorphism of F1,F2
for p being Element of the carrier of (Polynom-Ring F1) holds NormPolynomial ((PolyHom h) . p) = (PolyHom h) . (NormPolynomial p)
let h be Monomorphism of F1,F2; :: thesis: for p being Element of the carrier of (Polynom-Ring F1) holds NormPolynomial ((PolyHom h) . p) = (PolyHom h) . (NormPolynomial p)
let p be Element of the carrier of (Polynom-Ring F1); :: thesis: NormPolynomial ((PolyHom h) . p) = (PolyHom h) . (NormPolynomial p)
set q = NormPolynomial ((PolyHom h) . p);
set pp = (PolyHom h) . p;
set r = (PolyHom h) . (NormPolynomial p);

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

suppose p is zero ; :: thesis: NormPolynomial ((PolyHom h) . p) = (PolyHom h) . (NormPolynomial p)

then A: p = 0_. F1 by UPROOTS:def 5;
then NormPolynomial p = 0_. F1 by RING_4:22;
then B: (PolyHom h) . (NormPolynomial p) = 0_. F2 by FIELD_1:22;
(PolyHom h) . p = 0_. F2 by A, FIELD_1:22;
hence NormPolynomial ((PolyHom h) . p) = (PolyHom h) . (NormPolynomial p) by B, RING_4:22; :: thesis: verum

end;

suppose not p is zero ; :: thesis: NormPolynomial ((PolyHom h) . p) = (PolyHom h) . (NormPolynomial p)

then not LC p is zero ;
then B: p . ((len p) -' 1) <> 0. F1 by RATFUNC1:def 6;
deg ((PolyHom h) . p) = deg p by FIELD_1:31;
then deg p = (len ((PolyHom h) . p)) - 1 by HURWITZ:def 2;
then A: (len p) - 1 = (len ((PolyHom h) . p)) - 1 by HURWITZ:def 2;

now :: thesis: for n being Nat holds (NormPolynomial ((PolyHom h) . p)) . n = ((PolyHom h) . (NormPolynomial p)) . n

let n be Nat; :: thesis: (NormPolynomial ((PolyHom h) . p)) . n = ((PolyHom h) . (NormPolynomial p)) . n
reconsider i = n as Element of NAT by ORDINAL1:def 12;
((PolyHom h) . p) . i = h . (p . i) by FIELD_1:def 2;
then (NormPolynomial ((PolyHom h) . p)) . i = (h . (p . i)) / (((PolyHom h) . p) . ((len p) -' 1)) by A, POLYNOM5:def 11
.= (h . (p . i)) * ((h . (p . ((len p) -' 1))) ") by FIELD_1:def 2
.= (h . (p . i)) * (h . ((p . ((len p) -' 1)) ")) by B, FIELD_2:6
.= h . ((p . i) / (p . ((len p) -' 1))) by GROUP_6:def 6
.= h . ((NormPolynomial p) . i) by POLYNOM5:def 11
.= ((PolyHom h) . (NormPolynomial p)) . i by FIELD_1:def 2 ;
hence (NormPolynomial ((PolyHom h) . p)) . n = ((PolyHom h) . (NormPolynomial p)) . n ; :: thesis: verum

end;

hence NormPolynomial ((PolyHom h) . p) = (PolyHom h) . (NormPolynomial p) ; :: thesis: verum

end;

end;