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 )
A1: dom R = Y by PARTFUN1:def 2;
defpred S₁[ object , object ] means [$1,$2] in R;
A2: for x being object st x in Y holds
ex y being object st S₁[x,y] by XTUPLE_0:def 12, A1;
consider f being Function such that
A3: ( dom f = Y & ( for x being object st x in Y holds
S₁[x,f . x] ) ) from CLASSES1:sch 1(A2);
A4: f = { [x,(f . x)] where x is Element of dom f : x in dom f } by Th20;

A5: now :: thesis: for z being object st z in f holds
z in R

let z be object ; :: 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
A6: ( z = [x,(f . x)] & x in dom f ) by A4;
thus z in R by A6, A3; :: thesis: verum

end;

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