set g = canHom f;
set A = R / (ker f);
set B = Image f;
set I = ker f;

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

let x, y be object ; :: thesis: ( x in the carrier of (R / (ker f)) & y in the carrier of (R / (ker f)) & (canHom f) . x = (canHom f) . y implies x = y )
assume D: ( x in the carrier of (R / (ker f)) & y in the carrier of (R / (ker f)) & (canHom f) . x = (canHom f) . y ) ; :: thesis: x = y
then reconsider x1 = x, y1 = y as Element of (R / (ker f)) ;
consider a being Element of R such that
H1: x1 = Class ((EqRel (R,(ker f))),a) by RING_1:11;
consider b being Element of R such that
H2: y1 = Class ((EqRel (R,(ker f))),b) by RING_1:11;
H3: (canHom f) . x1 = f . a by H1, ch;
f . a = f . b by D, H3, H2, ch;
then 0. S = (f . a) - (f . b) by RLVECT_1:15
.= f . (a - b) by hom4 ;
then a - b in ker f ;
hence x = y by H1, H2, RING_1:6; :: thesis: verum

end;

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

now :: thesis: for x being object holds
( x in rng (canHom f) iff x in rng f )

let x be object ; :: thesis: ( x in rng (canHom f) iff x in rng f )

Y: now :: thesis: ( x in rng (canHom f) implies x in rng f )

assume x in rng (canHom f) ; :: thesis: x in rng f
then consider y being object such that
H1: ( y in dom (canHom f) & (canHom f) . y = x ) by FUNCT_1:def 3;
reconsider y = y as Element of (R / (ker f)) by H1;
consider a being Element of R such that
H2: y = Class ((EqRel (R,(ker f))),a) by RING_1:11;
H3: (canHom f) . y = f . a by H2, ch;
dom f = the carrier of R by FUNCT_2:def 1;
hence x in rng f by H1, H3, FUNCT_1:3; :: thesis: verum

end;

now :: thesis: ( x in rng f implies x in rng (canHom f) )

assume x in rng f ; :: thesis: x in rng (canHom f)
then consider a being object such that
H1: ( a in dom f & f . a = x ) by FUNCT_1:def 3;
reconsider a = a as Element of R by H1;
H2: (canHom f) . (Class ((EqRel (R,(ker f))),a)) = f . a by ch;
H3: dom (canHom f) = the carrier of (R / (ker f)) by FUNCT_2:def 1;
Class ((EqRel (R,(ker f))),a) is Element of (R / (ker f)) by RING_1:12;
hence x in rng (canHom f) by H3, H2, H1, FUNCT_1:3; :: thesis: verum

end;

hence ( x in rng (canHom f) iff x in rng f ) by Y; :: thesis: verum

end;

then rng (canHom f) = rng f by TARSKI:2;
then rng (canHom f) = the carrier of (Image f) by defim;
then canHom f is onto by FUNCT_2:def 3;
hence canHom f is RingEpimorphism ; :: thesis: verum