now :: thesis: for X being set st X in Class R holds

X <> {}

then consider g being Function such that 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;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

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

deffunc H
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;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

consider f being Function of D,(Class R) such that

A7: for x being Element of D holds f . x = H

reconsider g = g as Function of (Class R),D by A2, A4, FUNCT_2:def 1, RELSET_1:4;

deffunc H

consider bR being BinOp of (Class R) such that

A8: for x, y being Element of Class R holds bR . (x,y) = H

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 A9, A10;

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 A12, A13, EQREL_1:22;

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 A11, A15, EQREL_1:22;

then [(b . ((g . x9),(g . y9))),(b . (x19,y19))] in R by A1, A14, Def2;

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 A16, A17, EQREL_1:23; :: thesis: verum