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;

take uR = (f * u) * g; :: thesis: for x, y being set st x in Class R & y in x holds

uR . x = Class (R,(u . y))

let x, y be set ; :: thesis: ( x in Class R & y in x implies uR . x = Class (R,(u . y)) )

assume that

A8: x in Class R and

A9: y in x ; :: thesis: uR . x = Class (R,(u . y))

A10: D = dom (f * u) by FUNCT_2:def 1;

g . x in rng g by A2, A8, FUNCT_1:def 3;

then A11: (f * u) . (g . x) = f . (u . (g . x)) by A4, A10, FUNCT_1:12;

Class R = dom uR by FUNCT_2:def 1;

then A12: uR . x = (f * u) . (g . x) by A8, FUNCT_1:12;

reconsider x9 = x as Element of Class R by A8;

reconsider y9 = y as Element of D by A8, A9;

A13: ex x1 being object st

( x1 in D & x9 = Class (R,x1) ) by EQREL_1:def 3;

g . x9 in x by A3;

then [(g . x9),y9] in R by A9, A13, EQREL_1:22;

then [(u . (g . x9)),(u . y9)] in R by A1, Def1;

then A14: u . (g . x9) in EqClass (R,(u . y9)) by EQREL_1:19;

f . (u . (g . x9)) = EqClass (R,(u . (g . x9))) by A7;

hence uR . x = Class (R,(u . y)) by A12, A11, A14, EQREL_1:23; :: thesis: verum