let h be PartFunc of REAL , REAL ; :: thesis: ( rng h is bounded & upper_bound (rng h) = lower_bound (rng h) implies h is constant )
assume that
A1: rng h is bounded and
A2: upper_bound (rng h) = lower_bound (rng h) ; :: thesis: h is constant
assume not h is constant ; :: thesis: contradiction
then consider x1, x2 being set such that
A4: ( x1 in dom h & x2 in dom h & h . x1 <> h . x2 ) by FUNCT_1:def 16;
( h . x1 in rng h & h . x2 in rng h ) by A4, FUNCT_1:def 5;
hence contradiction by A1, A2, A4, SEQ_4:25; :: thesis: verum