let R be Ring; :: thesis: for S being R -monomorphic Ring
for f being Monomorphism of R,S
for a being Element of R holds
( f . a = 0. S iff a = 0. R )
let S be R -monomorphic Ring; :: thesis: for f being Monomorphism of R,S
for a being Element of R holds
( f . a = 0. S iff a = 0. R )
let f be Monomorphism of R,S; :: thesis: for a being Element of R holds
( f . a = 0. S iff a = 0. R )
let a be Element of R; :: thesis: ( f . a = 0. S iff a = 0. R )

now :: thesis: ( f . a = 0. S implies a = 0. R )

assume f . a = 0. S ; :: thesis: a = 0. R
then f . a = f . (0. R) by RING_2:6;
hence a = 0. R by FUNCT_2:19; :: thesis: verum

end;

hence ( f . a = 0. S iff a = 0. R ) by RING_2:6; :: thesis: verum