let X be set ; :: thesis: ( X <> {} implies for y being object ex f being Function st
( dom f = X & rng f = {y} ) )
assume A1: X <> {} ; :: thesis: for y being object ex f being Function st
( dom f = X & rng f = {y} )
let y be object ; :: thesis: ex f being Function st
( dom f = X & rng f = {y} )
deffunc H1( object ) -> object = y;
consider f being Function such that
A2: dom f = X and
A3: for x being object st x in X holds
f . x = H1(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 object holds
( y1 in rng f iff y1 = y )
proof
let y1 be object ; :: thesis: ( y1 in rng f iff y1 = y )
A4: now :: thesis: ( y1 = y implies y1 in rng f )
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, Def3; :: thesis: verum
end;
now :: thesis: ( y1 in rng f implies y1 = y )
assume y1 in rng f ; :: thesis: y1 = y
then ex x being object st
( x in dom f & y1 = f . x ) by Def3;
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