now :: thesis: for X being set st X in Class R holds
X <> {}
let X be set ; :: thesis: ( X in Class R implies X <> {} )
assume X in Class R ; :: thesis: X <> {}
then ex x being object st
( x in D & X = Class (R,x) ) by EQREL_1:def 3;
hence X <> {} by EQREL_1:20; :: thesis: verum
end;
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 H3( Element of D) -> Element of Class R = EqClass (R,\$1);
consider f being Function of D,() such that
A7: for x being Element of D holds f . x = H3(x) from reconsider g = g as Function of (),D by ;
deffunc H4( Element of Class R, Element of Class R) -> Element of Class R = f . (b . ((g . \$1),(g . \$2)));
consider bR being BinOp of () such that
A8: for x, y being Element of Class R holds bR . (x,y) = H4(x,y) from take bR ; :: thesis: for x, y, x1, y1 being set st x in Class R & y in Class R & x1 in x & y1 in y holds
bR . (x,y) = Class (R,(b . (x1,y1)))

let x, y, x1, y1 be set ; :: thesis: ( x in Class R & y in Class R & x1 in x & y1 in y implies bR . (x,y) = Class (R,(b . (x1,y1))) )
assume that
A9: x in Class R and
A10: y in Class R and
A11: x1 in x and
A12: y1 in y ; :: thesis: bR . (x,y) = Class (R,(b . (x1,y1)))
reconsider x9 = x, y9 = y as Element of Class R by ;
reconsider x19 = x1, y19 = y1 as Element of D by A9, A10, A11, A12;
A13: ex y2 being object st
( y2 in D & y9 = Class (R,y2) ) by EQREL_1:def 3;
g . y9 in y by A3;
then A14: [(g . y9),y19] in R by ;
A15: ex x2 being object st
( x2 in D & x9 = Class (R,x2) ) by EQREL_1:def 3;
g . x9 in x by A3;
then [(g . x9),x19] in R by ;
then [(b . ((g . x9),(g . y9))),(b . (x19,y19))] in R by ;
then A16: b . ((g . x9),(g . y9)) in EqClass (R,(b . (x19,y19))) by EQREL_1:19;
A17: f . (b . ((g . x9),(g . y9))) = EqClass (R,(b . ((g . x9),(g . y9)))) by A7;
bR . (x9,y9) = f . (b . ((g . x9),(g . y9))) by A8;
hence bR . (x,y) = Class (R,(b . (x1,y1))) by ; :: thesis: verum