:: deftheorem defines ContinuousFunctions C0SP3:def 3 :
for S, T being RealNormSpace holds ContinuousFunctions (S,T) = { f where f is Function of the carrier of S, the carrier of T : f is_continuous_on the carrier of S } ;