theorem :: FIELD_1:18

for R being Ring
for S being b₁ -homomorphic Ring
for h being Homomorphism of R,S holds h . (Product (<*> the carrier of R)) = 1. S