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