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 V8()

let h be PartFunc of W,REAL; :: thesis: ( rng h is real-bounded & upper_bound (rng h) = lower_bound (rng h) implies h is V8() )

assume A1: ( rng h is real-bounded & upper_bound (rng h) = lower_bound (rng h) ) ; :: thesis: h is V8()

assume h is V8() ; :: 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

h is V8()

let h be PartFunc of W,REAL; :: thesis: ( rng h is real-bounded & upper_bound (rng h) = lower_bound (rng h) implies h is V8() )

assume A1: ( rng h is real-bounded & upper_bound (rng h) = lower_bound (rng h) ) ; :: thesis: h is V8()

assume h is V8() ; :: 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