now :: thesis: for x being object st x in ContinuousFunctions (S,T) holds
x is Function

let x be object ; :: thesis: ( x in ContinuousFunctions (S,T) implies x is Function )
assume x in ContinuousFunctions (S,T) ; :: thesis: x is Function
then ex f being Function of S,(TopSpaceMetr T) st
( x = f & f is continuous ) ;
hence x is Function ; :: thesis: verum

end;

hence ( not ContinuousFunctions (S,T) is empty & ContinuousFunctions (S,T) is functional ) by FUNCT_1:def 13; :: thesis: verum