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
A3: ( h1 = |.h.| & h1 is continuous ) ;
( h1 is bounded_above & h1 is bounded_below ) by SEQ_2:def 8, A3;
then consider r1 being real number such that
A4: for y being set st y in dom h1 holds
h1 . y < r1 by SEQ_2:def 1;
A5: for y being set st y in dom h holds
abs (h . y) < r1

proof

let y be set ; :: thesis: ( y in dom h implies abs (h . y) < r1 )
assume A6: y in dom h ; :: thesis: abs (h . y) < r1
A7: dom h1 = dom h by A3, VALUED_1:def 11;
h1 . y = |.(h . y).| by A3, VALUED_1:18
.= abs (h . y) ;
hence abs (h . y) < r1 by A4, A6, A7; :: thesis: verum

end;

h is bounded by A5, SEQ_2:def 5;
then h | the carrier of X is bounded by FUNCT_2:33;
hence x in ComplexBoundedFunctions the carrier of X by A1; :: thesis: verum