let X be non empty TopSpace; :: thesis: for x being set st x in CC_0_Functions X holds
x in CContinuousFunctions X
let x be set ; :: thesis: ( x in CC_0_Functions X implies x in CContinuousFunctions X )
assume A1: x in CC_0_Functions X ; :: thesis: x in CContinuousFunctions X
consider f being Function of the carrier of X,COMPLEX 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 CContinuousFunctions X by A2; :: thesis: verum