set g = canHom f;
set A = R / (ker f);
set B = Image f;
set I = ker f;
now 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 = ylet x,
y be
object ;
( 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 )
;
x = ythen 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;
verum end;
then
canHom f is one-to-one
by FUNCT_2:19;
hence
canHom f is monomorphism
; canHom f is RingEpimorphism
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
; verum