ContinuousFunctions (S,T) c= BoundedFunctions ( the carrier of S,T) by Th34;
hence (BoundedFunctionsNorm ( the carrier of S,T)) | (ContinuousFunctions (S,T)) is Function of (ContinuousFunctions (S,T)),REAL by FUNCT_2:32; :: thesis: verum