let F1 be Field; :: thesis: for F2 being F1 -homomorphic Field
for h being Homomorphism of F1,F2
for a being Element of F1
for n being Nat holds (PolyHom h) . ((X- a) `^ n) = (X- (h . a)) `^ n
let F2 be F1 -homomorphic Field; :: thesis: for h being Homomorphism of F1,F2
for a being Element of F1
for n being Nat holds (PolyHom h) . ((X- a) `^ n) = (X- (h . a)) `^ n
let h be Homomorphism of F1,F2; :: thesis: for a being Element of F1
for n being Nat holds (PolyHom h) . ((X- a) `^ n) = (X- (h . a)) `^ n
let a be Element of F1; :: thesis: for n being Nat holds (PolyHom h) . ((X- a) `^ n) = (X- (h . a)) `^ n
let n be Nat; :: thesis: (PolyHom h) . ((X- a) `^ n) = (X- (h . a)) `^ n
defpred S₁[ Nat] means (PolyHom h) . ((X- a) `^ $1) = (X- (h . a)) `^ $1;
(PolyHom h) . ((X- a) `^ 0) = (PolyHom h) . (1_. F1) by POLYNOM5:15
.= 1_. F2 by FIELD_1:23
.= (X- (h . a)) `^ 0 by POLYNOM5:15 ;
then IA: S₁[ 0 ] ;

IS: now :: thesis: for k being Nat st S₁[k] holds
S₁[k + 1]

let k be Nat; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume IV: S₁[k] ; :: thesis: S₁[k + 1]
reconsider p = (X- a) `^ k, q = X- a as Element of the carrier of (Polynom-Ring F1) by POLYNOM3:def 10;
A: ( (PolyHom h) . p = (X- (h . a)) `^ k & (PolyHom h) . q = X- (h . a) ) by IV, FIELD_13:25;
(PolyHom h) . ((X- a) `^ (k + 1)) = (PolyHom h) . (((X- a) `^ k) *' (X- a)) by POLYNOM5:19
.= (PolyHom h) . (p * q) by POLYNOM3:def 10
.= ((PolyHom h) . p) * ((PolyHom h) . q) by FIELD_1:25
.= ((X- (h . a)) `^ k) *' (X- (h . a)) by A, POLYNOM3:def 10
.= (X- (h . a)) `^ (k + 1) by POLYNOM5:19 ;
hence S₁[k + 1] ; :: thesis: verum

end;

for k being Nat holds S₁[k] from NAT_1:sch 2(IA, IS);
hence (PolyHom h) . ((X- a) `^ n) = (X- (h . a)) `^ n ; :: thesis: verum