let X be non empty compact TopSpace; :: thesis: for x being set st x in ContinuousFunctions X holds
x in BoundedFunctions the carrier of X
let x be set ; :: thesis: ( x in ContinuousFunctions X implies x in BoundedFunctions the carrier of X )
assume x in ContinuousFunctions X ; :: thesis: x in BoundedFunctions the carrier of X
then consider h being continuous RealMap of X such that
A1: x = h ;
A2: ( h is bounded_above & h is bounded_below ) by SEQ_2:def 8;
then consider r1 being Real such that
A3: for y being object st y in dom h holds
h . y < r1 by SEQ_2:def 1;
A4: the carrier of X /\ (dom h) c= dom h by XBOOLE_1:17;
then for y being object st y in the carrier of X /\ (dom h) holds
h . y <= r1 by A3;
then A5: h | the carrier of X is bounded_above by RFUNCT_1:70;
consider r2 being Real such that
A6: for y being object st y in dom h holds
r2 < h . y by A2, SEQ_2:def 2;
for y being object st y in the carrier of X /\ (dom h) holds
r2 <= h . y by A4, A6;
then A7: h | the carrier of X is bounded_below by RFUNCT_1:71;
the carrier of X /\ the carrier of X = the carrier of X ;
then h | the carrier of X is bounded by A5, A7, RFUNCT_1:75;
hence x in BoundedFunctions the carrier of X by A1; :: thesis: verum