let Y be set ; :: thesis: for W being non empty set
for h being PartFunc of W,REAL st h .: Y is real-bounded & upper_bound (h .: Y) = lower_bound (h .: Y) holds
h | Y is constant
let W be non empty set ; :: thesis: for h being PartFunc of W,REAL st h .: Y is real-bounded & upper_bound (h .: Y) = lower_bound (h .: Y) holds
h | Y is constant
let h be PartFunc of W,REAL; :: thesis: ( h .: Y is real-bounded & upper_bound (h .: Y) = lower_bound (h .: Y) implies h | Y is constant )
rng (h | Y) = h .: Y by RELAT_1:115;
hence ( h .: Y is real-bounded & upper_bound (h .: Y) = lower_bound (h .: Y) implies h | Y is constant ) by Th18; :: thesis: verum