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 A1: ( rng h is bounded & 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
A2: ( x1 in dom h & x2 in dom h ) and
A3: h . x1 <> h . x2 by FUNCT_1:def 16;
( h . x1 in rng h & h . x2 in rng h ) by A2, FUNCT_1:def 5;
hence contradiction by A1, A3, SEQ_4:25; :: thesis: verum