set A = R / (ker f);
set B = Image f;
defpred S1[ 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) & S1[x,y] )
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
S1[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
; for a being Element of R holds g . (Class ((EqRel (R,(ker f))),a)) = f . a
hence
for a being Element of R holds g . (Class ((EqRel (R,(ker f))),a)) = f . a
; verum