theorem hcon: :: FIELD_8:13

for R being Ring
for S being b₁ -homomorphic Ring
for h being Homomorphism of R,S
for a being Element of R holds (PolyHom h) . (a | R) = (h . a) | S