let X be non empty TopSpace; :: thesis: for T being NormedLinearTopSpace
for x being set st x in C_0_Functions (X,T) holds
x in BoundedFunctions ( the carrier of X,T)
let T be NormedLinearTopSpace; :: thesis: for x being set st x in C_0_Functions (X,T) holds
x in BoundedFunctions ( the carrier of X,T)
let x be set ; :: thesis: ( x in C_0_Functions (X,T) implies x in BoundedFunctions ( the carrier of X,T) )
assume x in C_0_Functions (X,T) ; :: thesis: x in BoundedFunctions ( the carrier of X,T)
then consider f being Function of the carrier of X, the carrier of T such that
A2: ( f = x & f is continuous & ex Y being non empty Subset of X st
( Y is compact & Cl (support f) c= Y ) ) ;
consider Y being non empty Subset of X such that
A3: ( Y is compact & Cl (support f) c= Y ) by A2;
A4: dom f = the carrier of X by FUNCT_2:def 1;
then consider K being Real such that
A5: ( 0 <= K & ( for x being Point of X st x in Y holds
||.(f . x).|| <= K ) ) by A3, A2, Lm2;
for x being Element of X holds ||.(f . x).|| <= K
proof
let x be Element of X; :: thesis: ||.(f . x).|| <= K
A6: support f c= Cl (support f) by PRE_TOPC:18;
per cases ( not x in Y or x in Y ) ;
suppose not x in Y ; :: thesis: ||.(f . x).|| <= K
then not x in support f by A3, A6;
then ( not x in dom f or f /. x = 0. T ) by Def10;
hence ||.(f . x).|| <= K by A5, A4; :: thesis: verum
end;
suppose x in Y ; :: thesis: ||.(f . x).|| <= K
hence ||.(f . x).|| <= K by A5; :: thesis: verum
end;
end;
end;
then f is bounded by RSSPACE4:def 4, A5;
hence x in BoundedFunctions ( the carrier of X,T) by RSSPACE4:def 5, A2; :: thesis: verum