let W be non empty set ; :: thesis: for h being PartFunc of W,REAL st rng h is real-bounded & upper_bound (rng h) = lower_bound (rng h) holds
h is constant
let h be PartFunc of W,REAL; :: thesis: ( rng h is real-bounded & upper_bound (rng h) = lower_bound (rng h) implies h is constant )
assume A1: ( rng h is real-bounded & upper_bound (rng h) = lower_bound (rng h) ) ; :: thesis: h is constant
assume h is constant ; :: thesis: contradiction
then consider x1, x2 being object such that
A2: ( x1 in dom h & x2 in dom h ) and
A3: h . x1 <> h . x2 ;
( h . x1 in rng h & h . x2 in rng h ) by A2, FUNCT_1:def 3;
hence contradiction by A1, A3, SEQ_4:12; :: thesis: verum