let Y be set ; :: thesis: for R being Y -defined total Relation ex f being Function of Y,(rng R) st
( f c= R & dom f = Y )
set X = Y;
let R be Y -defined total Relation; :: thesis: ex f being Function of Y,(rng R) st
( f c= R & dom f = Y )
B0: dom R = Y by PARTFUN1:def 2;
defpred S₁[ set , set ] means [$1,$2] in R;
B1: for x being set st x in Y holds
ex y being set st S₁[x,y] by B0, RELAT_1:def 4;
consider f being Function such that
B2: ( dom f = Y & ( for x being set st x in Y holds
S₁[x,f . x] ) ) from CLASSES1:sch 1(B1);
B3: f = { [x,(f . x)] where x is Element of dom f : x in dom f } by Th20;

Z1: now

let z be set ; :: thesis: ( z in f implies z in R )
assume z in f ; :: thesis: z in R
then consider x being Element of dom f such that
C0: ( z = [x,(f . x)] & x in dom f ) by B3;
thus z in R by C0, B2; :: thesis: verum

end;

then f c= R by TARSKI:def 3;
then rng f c= rng R by RELAT_1:11;
then reconsider g = f as Function of Y,(rng R) by B2, FUNCT_2:67, RELSET_1:4;
take g ; :: thesis: ( g c= R & dom g = Y )
thus ( g c= R & dom g = Y ) by Z1, B2, TARSKI:def 3; :: thesis: verum