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 ;
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 ;
then A11: (f * u) . (g . x) = f . (u . (g . x)) by ;
Class R = dom uR by FUNCT_2:def 1;
then A12: uR . x = (f * u) . (g . x) by ;
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 ;
then [(u . (g . x9)),(u . y9)] in R by ;
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 ; :: thesis: verum