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