let X be non empty TopSpace; for x being set st x in CC_0_Functions X holds
x in ComplexBoundedFunctions the carrier of X
let x be set ; ( x in CC_0_Functions X implies x in ComplexBoundedFunctions the carrier of X )
assume A1:
x in CC_0_Functions X
; 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
A4:
( f1 = |.f.| & f1 is continuous )
;
f1 .: Y is compact
by A4, A3, JORDAN_A:1;
then reconsider Y1 = f1 .: Y as non empty real-bounded Subset of REAL by RCOMP_1:10;
A5:
Y1 c= [.(inf Y1),(sup Y1).]
by XXREAL_2:69;
reconsider r1 = inf Y1 as Real ;
reconsider r2 = sup Y1 as Real ;
consider r being Real such that
A6:
r = (|.r1.| + |.r2.|) + 1
;
for p being Element of Y holds
( r > 0 & - r < f1 . p & f1 . p < r )
then consider r being Real such that
A10:
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 )
then consider s1 being Real such that
A15:
for x being Point of X holds
( - s1 < f1 . x & f1 . x < s1 )
;
for y being object st y in the carrier of X /\ (dom f1) holds
f1 . y <= s1
by A15;
then A16:
f1 | the carrier of X is bounded_above
by RFUNCT_1:70;
for y being object st y in the carrier of X /\ (dom f1) holds
- s1 <= f1 . y
by A15;
then A17:
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 A16, A17, RFUNCT_1:75;
then
|.(f | the carrier of X).| is bounded
by A4, 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; verum