theorem Th4: :: FIELD_2:5

for R being Ring
for S being b₁ -monomorphic Ring
for f being Monomorphism of R,S
for a being Element of R holds
( f . a = 0. S iff a = 0. R )