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
deffunc H1( 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 = H1(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 H2( 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) = H2(x,y)
from STACKS_1:sch 2();
take
bR
; 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 ; ( 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
; 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; verum