for X being set st X in Class R holds
X <> {} ;
then consider g being Function such that
A2: dom g = Class R and
A3: for X being set st X in Class R holds
g . X in X by FUNCT_1:111;
A4: rng g c= D

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in rng g or x in D )
assume x in rng g ; :: thesis: x in D
then consider y being object such that
A5: y in dom g and
A6: x = g . y by FUNCT_1:def 3;
reconsider y = y as set by TARSKI:1;
x in y by A2, A3, A5, A6;
hence x in D by A2, A5; :: thesis: verum

end;

deffunc H₁( Element of D) -> Element of Class R = EqClass (R,$1);
consider f being Function of D,(Class R) such that
A7: for x being Element of D holds f . x = H₁(x) from FUNCT_2:sch 4();
reconsider g = g as Function of (Class R),D by A2, A4, FUNCT_2:def 1, RELSET_1:4;
deffunc H₂( Element of C, Element of Class R) -> Element of Class R = f . (b . ($1,(g . $2)));
consider bR being Function of [:C,(Class R):],(Class R) such that
A8: for x being Element of C
for y being Element of Class R holds bR . (x,y) = H₂(x,y) from STACKS_1:sch 2();
take bR ; :: thesis: for x, y, y1 being set st x in C & y in Class R & y1 in y holds
bR . (x,y) = Class (R,(b . (x,y1)))
let x, y, y1 be set ; :: thesis: ( x in C & y in Class R & y1 in y implies bR . (x,y) = Class (R,(b . (x,y1))) )
assume that
A9: x in C and
A10: y in Class R and
A11: y1 in y ; :: thesis: bR . (x,y) = Class (R,(b . (x,y1)))
reconsider x9 = x as Element of C by A9;
reconsider y9 = y as Element of Class R by A10;
reconsider y19 = y1 as Element of D by A10, A11;
A12: ex y2 being object st
( y2 in D & y9 = Class (R,y2) ) by EQREL_1:def 3;
g . y9 in y by A3;
then [(g . y9),y19] in R by A11, A12, EQREL_1:22;
then [(b . (x9,(g . y9))),(b . (x9,y19))] in R by A1, Def1;
then A13: b . (x9,(g . y9)) in EqClass (R,(b . (x9,y19))) by EQREL_1:19;
A14: f . (b . (x9,(g . y9))) = EqClass (R,(b . (x9,(g . y9)))) by A7;
bR . (x9,y9) = f . (b . (x9,(g . y9))) by A8;
hence bR . (x,y) = Class (R,(b . (x,y1))) by A13, A14, EQREL_1:23; :: thesis: verum