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

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

assume (f ") . a = 0. R ; :: thesis: a = 0. S
then f . (0. R) = a by FUNCT_1:35;
hence a = 0. S by RING_2:6; :: thesis: verum

end;

A2: dom f = [#] R by FUNCT_2:def 1;

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

assume a = 0. S ; :: thesis: (f ") . a = 0. R
then f . (0. R) = a by RING_2:6;
hence (f ") . a = 0. R by A2, FUNCT_1:34; :: thesis: verum

end;

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