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