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