let f be Function; :: thesis: ( ( not f is empty & f is constant ) iff ex y being object st rng f = {y} )

hereby :: thesis: ( ex y being object st rng f = {y} implies ( not f is empty & f is constant ) )

assume A1: ( not f is empty & f is constant ) ; :: thesis: ex y being object st rng f = {y}
set Y = the Element of rng f;
reconsider y = the Element of rng f as object ;
consider x being object such that
A2: ( x in dom f & f . x = y ) by A1, FUNCT_1:def 3;
take y = y; :: thesis: rng f = {y}

now :: thesis: for y2 being object st y2 in rng f holds
y2 in {y}

let y2 be object ; :: thesis: ( y2 in rng f implies y2 in {y} )
assume y2 in rng f ; :: thesis: y2 in {y}
then consider x2 being object such that
A3: ( x2 in dom f & f . x2 = y2 ) by FUNCT_1:def 3;
f . x = f . x2 by A1, A2, A3, FUNCT_1:def 10;
hence y2 in {y} by A2, A3, TARSKI:def 1; :: thesis: verum

end;

hence rng f = {y} by A1, TARSKI:def 3, ZFMISC_1:33; :: thesis: verum

end;

given y being object such that A4: rng f = {y} ; :: thesis: ( not f is empty & f is constant )
thus not f is empty by A4; :: thesis: f is constant

now :: thesis: for x1, x2 being object st x1 in dom f & x2 in dom f holds
f . x1 = f . x2

let x1, x2 be object ; :: thesis: ( x1 in dom f & x2 in dom f implies f . x1 = f . x2 )
assume ( x1 in dom f & x2 in dom f ) ; :: thesis: f . x1 = f . x2
then ( f . x1 in rng f & f . x2 in rng f ) by FUNCT_1:3;
then ( f . x1 = y & f . x2 = y ) by A4, TARSKI:def 1;
hence f . x1 = f . x2 ; :: thesis: verum

end;

hence f is constant by FUNCT_1:def 10; :: thesis: verum