for R, S being Ring
for f being Function of R,S st f is RingMonomorphism holds
for x being Element of R holds
( f . x = 0. S iff x = 0. R )