let X be non empty compact TopSpace; :: thesis: for x being set st x in CContinuousFunctions X holds
x in ComplexBoundedFunctions the carrier of X
let x be set ; :: thesis: ( x in CContinuousFunctions X implies x in ComplexBoundedFunctions the carrier of X )
assume x in CContinuousFunctions X ; :: thesis: x in ComplexBoundedFunctions the carrier of X
then consider h being continuous Function of the carrier of X,COMPLEX such that
A1: x = h ;
( |.h.| is Function of the carrier of X,REAL & |.h.| is continuous ) by Th8;
then consider h1 being Function of the carrier of X,REAL such that
A2: ( h1 = |.h.| & h1 is continuous ) ;
( h1 is bounded_above & h1 is bounded_below ) by A2, SEQ_2:def 8;
then consider r1 being Real such that
A3: for y being object st y in dom h1 holds
h1 . y < r1 by SEQ_2:def 1;
A4: for y being set st y in dom h holds
|.(h . y).| < r1
proof
let y be set ; :: thesis: ( y in dom h implies |.(h . y).| < r1 )
assume A5: y in dom h ; :: thesis: |.(h . y).| < r1
A6: dom h1 = dom h by A2, VALUED_1:def 11;
h1 . y = |.(h . y).| by A2, VALUED_1:18
.= |.(h . y).| ;
hence |.(h . y).| < r1 by A3, A5, A6; :: thesis: verum
end;
h is bounded by A4, COMSEQ_2:def 3;
then h | the carrier of X is bounded by FUNCT_2:33;
hence x in ComplexBoundedFunctions the carrier of X by A1; :: thesis: verum