X --> 0c in { f where f is continuous Function of the carrier of X,COMPLEX : verum } ;
hence not CContinuousFunctions X is empty ; :: thesis: verum