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

proof

let x be object ; :: thesis: ( x in the carrier of R implies ex y being object st
( y in the carrier of (R / I) & S₁[x,y] ) )
assume x in the carrier of R ; :: thesis: ex y being object st
( y in the carrier of (R / I) & S₁[x,y] )
then reconsider a = x as Element of R ;
reconsider y = Class ((EqRel (R,I)),a) as Element of (R / I) by RING_1:12;
take y ; :: thesis: ( y in the carrier of (R / I) & S₁[x,y] )
thus ( y in the carrier of (R / I) & S₁[x,y] ) ; :: thesis: verum

end;

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