C_0_Functions (X,T) c= BoundedFunctions ( the carrier of X,T) by Th60;
hence (BoundedFunctionsNorm ( the carrier of X,T)) | (C_0_Functions (X,T)) is Function of (C_0_Functions (X,T)),REAL by FUNCT_2:32; :: thesis: verum