let X be set ; :: thesis: ( X <> {} implies for y being set ex f being Function st
( dom f = X & rng f = {y} ) )
assume A1: X <> {} ; :: thesis: for y being set ex f being Function st
( dom f = X & rng f = {y} )
let y be set ; :: thesis: ex f being Function st
( dom f = X & rng f = {y} )
deffunc H₁( set ) -> set = y;
consider f being Function such that
A2: dom f = X and
A3: for x being set st x in X holds
f . x = H₁(x) from FUNCT_1:sch 3();
take f ; :: thesis: ( dom f = X & rng f = {y} )
thus dom f = X by A2; :: thesis: rng f = {y}
for y1 being set holds
( y1 in rng f iff y1 = y )

proof

let y1 be set ; :: thesis: ( y1 in rng f iff y1 = y )

A4: now

set x = the Element of X;
assume A5: y1 = y ; :: thesis: y1 in rng f
f . the Element of X = y by A1, A3;
hence y1 in rng f by A1, A2, A5, Def5; :: thesis: verum

end;

now

assume y1 in rng f ; :: thesis: y1 = y
then ex x being set st
( x in dom f & y1 = f . x ) by Def5;
hence y1 = y by A2, A3; :: thesis: verum

end;

hence ( y1 in rng f iff y1 = y ) by A4; :: thesis: verum

end;

hence rng f = {y} by TARSKI:def 1; :: thesis: verum