X --> 0 in { f where f is continuous RealMap of X : verum } ;
hence not ContinuousFunctions X is empty ; :: thesis: verum