for x being set st x in ContinuousFunctions X holds
x in BoundedFunctions the carrier of X by LMX01;
then ContinuousFunctions X c= BoundedFunctions the carrier of X by TARSKI:def 3;
hence (BoundedFunctionsNorm the carrier of X) | (ContinuousFunctions X) is Function of (ContinuousFunctions X),REAL by FUNCT_2:38; :: thesis: verum