let X be non empty TopSpace; :: thesis: for x being set st x in CC_0_Functions X holds
x in ComplexBoundedFunctions the carrier of X
let x be set ; :: thesis: ( x in CC_0_Functions X implies x in ComplexBoundedFunctions the carrier of X )
assume A1: x in CC_0_Functions X ; :: thesis: x in ComplexBoundedFunctions the carrier of X
consider f being Function of the carrier of X,COMPLEX 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;
( |.f.| is Function of the carrier of X,REAL & |.f.| is continuous ) by Th8, A2;
then consider f1 being Function of the carrier of X,REAL such that
A5: ( f1 = |.f.| & f1 is continuous ) ;
f1 .: Y is compact by JORDAN_A:1, A5, A3;
then reconsider Y1 = f1 .: Y as bounded Subset of REAL by RCOMP_1:10;
A6: Y1 c= [.(lower_bound Y1),(upper_bound Y1).] by TOPREAL6:18;
reconsider r1 = lower_bound Y1 as real number ;
reconsider r2 = upper_bound Y1 as real number ;
consider r being real number such that
A7: r = ((abs r1) + (abs r2)) + 1 ;
for p being Element of Y holds
( r > 0 & - r < f1 . p & f1 . p < r )

proof

let p be Element of Y; :: thesis: ( r > 0 & - r < f1 . p & f1 . p < r )
f1 . p in Y1 by FUNCT_2:35;
then f1 . p in [.r1,r2.] by A6;
then f1 . p in { t where t is Real : ( r1 <= t & t <= r2 ) } by RCOMP_1:def 1;
then consider r3 being Element of REAL such that
A8: ( r3 = f1 . p & r1 <= r3 & r3 <= r2 ) ;
- (abs r1) <= r1 by ABSVALUE:4;
then (- (abs r1)) - (abs r2) <= r1 - 0 by XREAL_1:13;
then ((- (abs r1)) - (abs r2)) - 1 < r1 - 0 by XREAL_1:15;
then A9: - r < r1 by A7;
r2 <= abs r2 by ABSVALUE:4;
then r2 + 0 <= (abs r2) + (abs r1) by XREAL_1:7;
then A10: r2 < r by A7, XREAL_1:8;
- r < f1 . p by A8, A9, XXREAL_0:2;
hence ( r > 0 & - r < f1 . p & f1 . p < r ) by A8, A10, XXREAL_0:2; :: thesis: verum

end;

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

proof

let x be Point of X; :: thesis: ( - r < f1 . x & f1 . x < r )
A14: ( x in the carrier of X \ Y or x in Y ) by XBOOLE_0:def 5;

per cases ( x in the carrier of X \ Y or x in Y ) by A14;

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

then A15: ( x in the carrier of X & not x in Y ) by XBOOLE_0:def 5;
Cl A is Subset of Y by A3;
then A16: Cl A c= Y ;
support f c= Cl A by PRE_TOPC:18;
then support f c= Y by A16, XBOOLE_1:1;
then A17: not x in support f by A15;
f . x = 0 by PRE_POLY:def 7, A17;
then |.(f . x).| = 0 ;
then f1 . x = 0 by A5, VALUED_1:18;
hence ( - r < f1 . x & f1 . x < r ) by A12; :: thesis: verum

end;

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

hence ( - r < f1 . x & f1 . x < r ) by A12; :: thesis: verum

end;

end;

end;

then consider s1 being real number such that
A21: for x being Point of X holds
( - s1 < f1 . x & f1 . x < s1 ) ;
for y being set st y in the carrier of X /\ (dom f1) holds
f1 . y <= s1 by A21;
then A22: f1 | the carrier of X is bounded_above by RFUNCT_1:70;
for y being set st y in the carrier of X /\ (dom f1) holds
- s1 <= f1 . y by A21;
then A23: f1 | the carrier of X is bounded_below by RFUNCT_1:71;
the carrier of X /\ the carrier of X = the carrier of X ;
then f1 | the carrier of X is bounded by RFUNCT_1:75, A22, A23;
then |.(f | the carrier of X).| is bounded by A5, RFUNCT_1:46;
then f | the carrier of X is bounded by CFUNCT_1:85;
hence x in ComplexBoundedFunctions the carrier of X by A2; :: thesis: verum