let S be non empty compact TopSpace; :: thesis: for T being NormedLinearTopSpace
for x being set st x in ContinuousFunctions (S,T) holds
x in BoundedFunctions ( the carrier of S,T)
let T be NormedLinearTopSpace; :: thesis: for x being set st x in ContinuousFunctions (S,T) holds
x in BoundedFunctions ( the carrier of S,T)
let x be set ; :: thesis: ( x in ContinuousFunctions (S,T) implies x in BoundedFunctions ( the carrier of S,T) )
assume x in ContinuousFunctions (S,T) ; :: thesis: x in BoundedFunctions ( the carrier of S,T)
then consider f being Function of the carrier of S, the carrier of T such that
A1: ( x = f & f is continuous ) ;
A2: dom f = the carrier of S by FUNCT_2:def 1;
consider K being Real such that
A3: ( 0 <= K & ( for x being Element of S st x in [#] S holds
||.(f . x).|| <= K ) ) by A1, A2, Lm2, COMPTS_1:1;
for x being Element of S holds ||.(f . x).|| <= K by A3;
then f is bounded by RSSPACE4:def 4, A3;
hence x in BoundedFunctions ( the carrier of S,T) by RSSPACE4:def 5, A1; :: thesis: verum