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 ContinuousFunctions (X,T)
let T be NormedLinearTopSpace; :: thesis: for x being set st x in C_0_Functions (X,T) holds
x in ContinuousFunctions (X,T)
let x be set ; :: thesis: ( x in C_0_Functions (X,T) implies x in ContinuousFunctions (X,T) )
assume x in C_0_Functions (X,T) ; :: thesis: x in ContinuousFunctions (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 ) ) ;
thus x in ContinuousFunctions (X,T) by A2; :: thesis: verum