theorem aXn: :: FIELD_15:34

for F1 being Field
for F2 being b₁ -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