set A = R / (ker f);
set B = Image f;
defpred S₁[ object , object ] means for a being Element of R st $1 = Class ((EqRel (R,(ker f))),a) holds
$2 = f . a;
X: for x being object st x in the carrier of (R / (ker f)) holds
ex y being object st
( y in the carrier of (Image f) & S₁[x,y] )

proof

let x be object ; :: thesis: ( x in the carrier of (R / (ker f)) implies ex y being object st
( y in the carrier of (Image f) & S₁[x,y] ) )
assume x in the carrier of (R / (ker f)) ; :: thesis: ex y being object st
( y in the carrier of (Image f) & S₁[x,y] )
then reconsider x1 = x as Element of (R / (ker f)) ;
consider b being Element of R such that
X1: x1 = Class ((EqRel (R,(ker f))),b) by RING_1:11;
take f . b ; :: thesis: ( f . b in the carrier of (Image f) & S₁[x,f . b] )
dom f = the carrier of R by FUNCT_2:def 1;
then f . b in rng f by FUNCT_1:3;
hence f . b in the carrier of (Image f) by defim; :: thesis: S₁[x,f . b]

now :: thesis: for a being Element of R st x = Class ((EqRel (R,(ker f))),a) holds
f . b = f . a

let a be Element of R; :: thesis: ( x = Class ((EqRel (R,(ker f))),a) implies f . b = f . a )
assume x = Class ((EqRel (R,(ker f))),a) ; :: thesis: f . b = f . a
then 0. S = f . (a - b) by ker1, X1, RING_1:6
.= (f . a) - (f . b) by hom4 ;
hence f . b = f . a by RLVECT_1:21; :: thesis: verum

end;

hence S₁[x,f . b] ; :: thesis: verum

end;

ex g being Function of (R / (ker f)),(Image f) st
for x being object st x in the carrier of (R / (ker f)) holds
S₁[x,g . x] from FUNCT_2:sch 1(X);
then consider g being Function of (R / (ker f)),(Image f) such that
Y: for x being object st x in the carrier of (R / (ker f)) holds
for a being Element of R st x = Class ((EqRel (R,(ker f))),a) holds
g . x = f . a ;
take g ; :: thesis: for a being Element of R holds g . (Class ((EqRel (R,(ker f))),a)) = f . a

now :: thesis: for a being Element of R holds g . (Class ((EqRel (R,(ker f))),a)) = f . a

let a be Element of R; :: thesis: g . (Class ((EqRel (R,(ker f))),a)) = f . a
reconsider x = Class ((EqRel (R,(ker f))),a) as Element of (R / (ker f)) by RING_1:12;
x in the carrier of (R / (ker f)) ;
hence g . (Class ((EqRel (R,(ker f))),a)) = f . a by Y; :: thesis: verum

end;

hence for a being Element of R holds g . (Class ((EqRel (R,(ker f))),a)) = f . a ; :: thesis: verum