set f = the carrier of S --> (0. T);
reconsider f = the carrier of S --> (0. T) as Function of the carrier of S, the carrier of T ;
f is_continuous_on the carrier of S by Th10;
then f in ContinuousFunctions (S,T) ;
hence not ContinuousFunctions (S,T) is empty ; :: thesis: ContinuousFunctions (S,T) is functional
for x being object st x in ContinuousFunctions (S,T) holds
x is Function

proof

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 the carrier of S, the carrier of T st
( x = f & f is_continuous_on the carrier of S ) ;
hence x is Function ; :: thesis: verum

end;

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