let R, S be Ring; :: thesis: 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 )
let f be Function of R,S; :: thesis: ( f is RingMonomorphism implies for x being Element of R holds
( f . x = 0. S iff x = 0. R ) )
assume A1: f is RingMonomorphism ; :: thesis: for x being Element of R holds
( f . x = 0. S iff x = 0. R )
then A2: f is RingHomomorphism ;
let x be Element of R; :: thesis: ( f . x = 0. S iff x = 0. R )
A3: f is one-to-one by A1;
( f . x = 0. S implies x = 0. R )
proof
assume A4: f . x = 0. S ; :: thesis: x = 0. R
f . (0. R) = 0. S by A2, Th50;
hence x = 0. R by A3, A4, FUNCT_2:19; :: thesis: verum
end;
hence ( f . x = 0. S iff x = 0. R ) by A2, Th50; :: thesis: verum