let X be non empty TopSpace; :: thesis: for x being set st x in C_0_Functions X holds
x in ContinuousFunctions X
let x be set ; :: thesis: ( x in C_0_Functions X implies x in ContinuousFunctions X )
assume A1: x in C_0_Functions X ; :: thesis: x in ContinuousFunctions X
consider f being RealMap of X such that
A2: ( f = x & f is continuous & ex Y being non empty Subset of X st
( Y is compact & ( for A being Subset of X st A = support f holds
Cl A is Subset of Y ) ) ) by A1;
thus x in ContinuousFunctions X by A2; :: thesis: verum