let Y be set ; :: thesis: for h being PartFunc of REAL,REAL st h .: Y is bounded & upper_bound (h .: Y) = lower_bound (h .: Y) holds
h | Y is constant
let h be PartFunc of REAL,REAL; :: thesis: ( h .: Y is bounded & upper_bound (h .: Y) = lower_bound (h .: Y) implies h | Y is constant )
set Z = h .: Y;
A1: rng (h | Y) = h .: Y by RELAT_1:115;
assume ( h .: Y is bounded & upper_bound (h .: Y) = lower_bound (h .: Y) ) ; :: thesis: h | Y is constant
hence h | Y is constant by A1, Th41; :: thesis: verum