let X, Y be non empty set ; :: thesis: for f being Function of X,Y holds
( f is constant iff ex y being Element of Y st rng f = {y} )
let f be Function of X,Y; :: thesis: ( f is constant iff ex y being Element of Y st rng f = {y} )

hereby :: thesis: ( ex y being Element of Y st rng f = {y} implies f is constant )

consider x being object such that
A1: x in dom f by XBOOLE_0:def 1;
set y = f . x;
reconsider y = f . x as Element of Y by A1, Th5;
assume A2: f is constant ; :: thesis: ex y being Element of Y st rng f = {y}
take y = y; :: thesis: rng f = {y}
for y9 being object holds
( y9 in rng f iff y9 = y )

proof

let y9 be object ; :: thesis: ( y9 in rng f iff y9 = y )

hereby :: thesis: ( y9 = y implies y9 in rng f )

assume y9 in rng f ; :: thesis: y9 = y
then ex x9 being object st
( x9 in dom f & y9 = f . x9 ) by FUNCT_1:def 3;
hence y9 = y by A2, A1; :: thesis: verum

end;

assume y9 = y ; :: thesis: y9 in rng f
hence y9 in rng f by A1, Th4; :: thesis: verum

end;

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

end;

given y being Element of Y such that A3: rng f = {y} ; :: thesis: f is constant
let x, x9 be object ; :: according to FUNCT_1:def 10 :: thesis: ( not x in proj1 f or not x9 in proj1 f or f . x = f . x9 )
assume x in dom f ; :: thesis: ( not x9 in proj1 f or f . x = f . x9 )
then A4: f . x in rng f by Th4;
assume x9 in dom f ; :: thesis: f . x = f . x9
then A5: f . x9 in rng f by Th4;
thus f . x = y by A3, A4, TARSKI:def 1
.= f . x9 by A3, A5, TARSKI:def 1 ; :: thesis: verum