let X, Y 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 :: thesis: ( X <> {} implies ex f being Function st
( dom f = X & rng f c= Y ) )

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

proof

let z be object ; :: thesis: ( z in rng f implies z in Y )
assume z in rng f ; :: thesis: z in Y
then ex x being object st
( x in dom f & z = f . x ) by Def3;
hence z in Y by A5, A3, A4; :: thesis: verum

end;

hence rng f c= Y ; :: thesis: verum

end;

now :: thesis: ( X = {} implies ex f being set st
( dom f = X & rng f c= Y ) )

assume A6: 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 A6; :: thesis: rng f c= Y
thus rng f c= Y ; :: thesis: verum

end;

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