set A = { f where f is Function of the carrier of S, the carrier of T : f is_continuous_on the carrier of S } ;
{ f where f is Function of the carrier of S, the carrier of T : f is_continuous_on the carrier of S } c= Funcs ( the carrier of S, the carrier of T)

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { f where f is Function of the carrier of S, the carrier of T : f is_continuous_on the carrier of S } or x in Funcs ( the carrier of S, the carrier of T) )
assume x in { f where f is Function of the carrier of S, the carrier of T : f is_continuous_on the carrier of S } ; :: thesis: x in Funcs ( the carrier of S, the carrier of T)
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 in Funcs ( the carrier of S, the carrier of T) by FUNCT_2:8; :: thesis: verum

end;

hence { f where f is Function of the carrier of S, the carrier of T : f is_continuous_on the carrier of S } is Subset of (RealVectSpace ( the carrier of S,T)) ; :: thesis: verum