let Y be set ; :: thesis: for h being PartFunc of REAL , REAL st Y c= dom h & 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: ( Y c= dom h & h .: Y is bounded & upper_bound (h .: Y) = lower_bound (h .: Y) implies h | Y is constant )
set Z = h .: Y;
assume that
A1: ( Y c= dom h & h .: Y is bounded ) and
A2: upper_bound (h .: Y) = lower_bound (h .: Y) ; :: thesis: h | Y is constant
A4: rng (h | Y) is bounded by A1, RELAT_1:148;
rng (h | Y) = h .: Y by RELAT_1:148;
hence h | Y is constant by A4, Th41, A2; :: thesis: verum