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 )

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

proof

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

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

assume y' in rng f ; :: thesis: y' = y
then consider x' being set such that
A3: ( x' in dom f & y' = f . x' ) by FUNCT_1:def 5;
thus y' = y by A3, A2, A1, FUNCT_1:def 16; :: thesis: verum

end;

assume y' = y ; :: thesis: y' in rng f
hence y' in rng f by A2, Th6; :: thesis: verum

end;

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

end;

given y being Element of Y such that A4: rng f = {y} ; :: thesis: f is constant
let x, x' be set ; :: according to FUNCT_1:def 16 :: thesis: ( not x in dom f or not x' in dom f or f . x = f . x' )
assume A5: x in dom f ; :: thesis: ( not x' in dom f or f . x = f . x' )
assume A6: x' in dom f ; :: thesis: f . x = f . x'
A7: ( f . x in rng f & f . x' in rng f ) by A5, A6, Th6;
hence f . x = y by A4, TARSKI:def 1
.= f . x' by A4, A7, TARSKI:def 1 ;
:: thesis: verum