let R be Ring; :: thesis: for S being R -homomorphic Ring
for f being Homomorphism of R,S holds
( f is monomorphism iff ker f = {(0. R)} )
let S be R -homomorphic Ring; :: thesis: for f being Homomorphism of R,S holds
( f is monomorphism iff ker f = {(0. R)} )
let f be Homomorphism of R,S; :: thesis: ( f is monomorphism iff ker f = {(0. R)} )

A: now :: thesis: ( f is monomorphism implies ker f = {(0. R)} )

assume B: f is monomorphism ; :: thesis: ker f = {(0. R)}
for x being object holds
( x in ker f iff x = 0. R )

proof

let x be object ; :: thesis: ( x in ker f iff x = 0. R )

C: now :: thesis: ( x in ker f implies x = 0. R )

assume AS: x in ker f ; :: thesis: x = 0. R
then reconsider a = x as Element of R ;
f . a = 0. S by AS, ker1
.= f . (0. R) by hom1 ;
hence x = 0. R by B, FUNCT_2:19; :: thesis: verum

end;

now :: thesis: ( x = 0. R implies x in ker f )

assume AS: x = 0. R ; :: thesis: x in ker f
then reconsider a = x as Element of R ;
f . a = 0. S by AS, hom1;
hence x in ker f ; :: thesis: verum

end;

hence ( x in ker f iff x = 0. R ) by C; :: thesis: verum

end;

hence ker f = {(0. R)} by TARSKI:def 1; :: thesis: verum

end;

now :: thesis: ( ker f = {(0. R)} implies f is monomorphism )

assume AS: ker f = {(0. R)} ; :: thesis: f is monomorphism

now :: thesis: for x, y being object st x in the carrier of R & y in the carrier of R & f . x = f . y holds
x = y

let x, y be object ; :: thesis: ( x in the carrier of R & y in the carrier of R & f . x = f . y implies x = y )
assume AS1: ( x in the carrier of R & y in the carrier of R & f . x = f . y ) ; :: thesis: x = y
then reconsider a = x, b = y as Element of R ;
0. S = (f . a) - (f . b) by AS1, RLVECT_1:15
.= f . (a - b) by hom4 ;
then a - b in ker f ;
then 0. R = a + (- b) by AS, TARSKI:def 1;
then a = - (- b) by RLVECT_1:6
.= b ;
hence x = y ; :: thesis: verum

end;

then f is one-to-one by FUNCT_2:19;
hence f is monomorphism ; :: thesis: verum

end;

hence ( f is monomorphism iff ker f = {(0. R)} ) by A; :: thesis: verum