set g = canHom I;
set B = R / I;

now :: thesis: for x being object holds
( x in rng (canHom I) iff x in the carrier of (R / I) )

let x be object ; :: thesis: ( x in rng (canHom I) iff x in the carrier of (R / I) )

now :: thesis: ( x in the carrier of (R / I) implies x in rng (canHom I) )

assume x in the carrier of (R / I) ; :: thesis: x in rng (canHom I)
then consider a being Element of R such that
H1: x = Class ((EqRel (R,I)),a) by RING_1:11;
H2: (canHom I) . a = x by H1, defhomI;
dom (canHom I) = the carrier of R by FUNCT_2:def 1;
hence x in rng (canHom I) by H2, FUNCT_1:def 3; :: thesis: verum

end;

hence ( x in rng (canHom I) iff x in the carrier of (R / I) ) ; :: thesis: verum

end;

then canHom I is onto by FUNCT_2:def 3, TARSKI:2;
hence canHom I is RingEpimorphism ; :: thesis: verum