let X be non empty set ; :: thesis: R_Normed_Algebra_of_BoundedFunctions X is RealBanachSpace
for seq being sequence of (R_Normed_Algebra_of_BoundedFunctions X) st seq is CCauchy holds
seq is convergent by Th36;
hence R_Normed_Algebra_of_BoundedFunctions X is RealBanachSpace by LOPBAN_1:def 16; :: thesis: verum