let X be non empty set ; :: thesis: for Y being ComplexBanachSpace holds C_NormSpace_of_BoundedFunctions X,Y is ComplexBanachSpace
let Y be ComplexBanachSpace; :: thesis: C_NormSpace_of_BoundedFunctions X,Y is ComplexBanachSpace
for seq being sequence of (C_NormSpace_of_BoundedFunctions X,Y) st seq is CCauchy holds
seq is convergent by Th29;
hence C_NormSpace_of_BoundedFunctions X,Y is ComplexBanachSpace by CLOPBAN1:def 14; :: thesis: verum