for x being object st x in ContinuousFunctions X holds
x in BoundedFunctions the carrier of X by Lm1;
then ContinuousFunctions X c= BoundedFunctions the carrier of X ;
hence (BoundedFunctionsNorm the carrier of X) | (ContinuousFunctions X) is Function of (ContinuousFunctions X),REAL by FUNCT_2:32; :: thesis: verum