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 Cauchy_sequence_by_Norm holds
seq is convergent by Th26;
hence C_NormSpace_of_BoundedFunctions (X,Y) is ComplexBanachSpace by CLOPBAN1:def 13; :: thesis: verum