let Y, X be set ; :: thesis: ( ( Y <> {} or X = {} ) implies ex f being Function st
( X = dom f & rng f c= Y ) )
assume A1: ( Y <> {} or X = {} ) ; :: thesis: ex f being Function st
( X = dom f & rng f c= Y )

A2: now

assume A3: X = {} ; :: thesis: ex f being set st
( dom f = X & rng f c= Y )
take f = {} ; :: thesis: ( dom f = X & rng f c= Y )
thus dom f = X by A3; :: thesis: rng f c= Y
thus rng f c= Y by XBOOLE_1:2; :: thesis: verum

end;

now

assume A4: X <> {} ; :: thesis: ex f being Function st
( dom f = X & rng f c= Y )
consider y being Element of Y;
A5: y in Y by A1, A4;
deffunc H₁( set ) -> Element of Y = y;
consider f being Function such that
A6: dom f = X and
A7: for x being set st x in X holds
f . x = H₁(x) from FUNCT_1:sch 3();
take f = f; :: thesis: ( dom f = X & rng f c= Y )
thus dom f = X by A6; :: thesis: rng f c= Y
for z being set st z in rng f holds
z in Y

proof

let z be set ; :: thesis: ( z in rng f implies z in Y )
assume z in rng f ; :: thesis: z in Y
then ex x being set st
( x in dom f & z = f . x ) by Def5;
hence z in Y by A5, A6, A7; :: thesis: verum

end;

hence rng f c= Y by TARSKI:def 3; :: thesis: verum

end;

hence ex f being Function st
( X = dom f & rng f c= Y ) by A2; :: thesis: verum