let X be non empty TopSpace; :: thesis: for x being set st x in C_0_Functions X holds
x in BoundedFunctions the carrier of X
let x be set ; :: thesis: ( x in C_0_Functions X implies x in BoundedFunctions the carrier of X )
assume A1: x in C_0_Functions X ; :: thesis: x in BoundedFunctions the carrier of X
consider f being RealMap of X such that
A2: ( f = x & f is continuous & ex Y being non empty Subset of X st
( Y is compact & ( for A being Subset of X st A = support f holds
Cl A is Subset of Y ) ) ) by A1;
consider Y being non empty Subset of X such that
A3: ( Y is compact & ( for A being Subset of X st A = support f holds
Cl A is Subset of Y ) ) by A2;
dom f = the carrier of X by FUNCT_2:def 1;
then reconsider A = support f as Subset of X by PRE_POLY:37;
reconsider Y1 = f .: Y as bounded Subset of REAL by A2, A3, JORDAN_A:1, RCOMP_1:10;
A5: Y1 c= [.(lower_bound Y1),(upper_bound Y1).] by TOPREAL6:18;
reconsider r1 = lower_bound Y1, r2 = upper_bound Y1 as real number ;
consider r being real number such that
A6: r = ((abs r1) + (abs r2)) + 1 ;
for p being Element of Y holds
( r > 0 & - r < f . p & f . p < r )

proof

let p be Element of Y; :: thesis: ( r > 0 & - r < f . p & f . p < r )
f . p in Y1 by FUNCT_2:35;
then f . p in [.r1,r2.] by A5;
then consider r3 being Element of REAL such that
A8: ( r3 = f . p & r1 <= r3 & r3 <= r2 ) ;
A9: ( abs r1 >= 0 & abs r2 >= 0 ) by COMPLEX1:46;
- (abs r1) <= r1 by ABSVALUE:4;
then (- (abs r1)) - (abs r2) <= r1 - 0 by A9, XREAL_1:13;
then ((- (abs r1)) - (abs r2)) - 1 < r1 - 0 by XREAL_1:15;
then A11: - r < r1 by A6;
r2 <= abs r2 by ABSVALUE:4;
then r2 + 0 <= (abs r2) + (abs r1) by A9, XREAL_1:7;
then r2 < r by A6, XREAL_1:8;
hence ( r > 0 & - r < f . p & f . p < r ) by A8, A11, XXREAL_0:2; :: thesis: verum

end;

then consider r being real number such that
A14: for p being Element of Y holds
( r > 0 & - r < f . p & f . p < r ) ;
for x being Point of X holds
( - r < f . x & f . x < r )

proof

let x be Point of X; :: thesis: ( - r < f . x & f . x < r )

per cases ( x in the carrier of X \ Y or x in Y ) by XBOOLE_0:def 5;

suppose A17: x in the carrier of X \ Y ; :: thesis: ( - r < f . x & f . x < r )

d: Cl A is Subset of Y by A3;
support f c= Cl A by PRE_TOPC:18;
then support f c= Y by d, XBOOLE_1:1;
then not x in support f by A17, XBOOLE_0:def 5;
then A21: f . x = 0 by PRE_POLY:def 7;
(- 1) * r < (- 1) * 0 by A14, XREAL_1:69;
hence ( - r < f . x & f . x < r ) by A21; :: thesis: verum

end;

suppose x in Y ; :: thesis: ( - r < f . x & f . x < r )

hence ( - r < f . x & f . x < r ) by A14; :: thesis: verum

end;

end;

end;

then consider s1 being real number such that
A24: for x being Point of X holds
( - s1 < f . x & f . x < s1 ) ;
for y being set st y in the carrier of X /\ (dom f) holds
f . y <= s1 by A24;
then A26: f | the carrier of X is bounded_above by RFUNCT_1:70;
for y being set st y in the carrier of X /\ (dom f) holds
- s1 <= f . y by A24;
then A27: f | the carrier of X is bounded_below by RFUNCT_1:71;
the carrier of X /\ the carrier of X = the carrier of X ;
then f | the carrier of X is bounded by A26, A27, RFUNCT_1:75;
hence x in BoundedFunctions the carrier of X by A2; :: thesis: verum