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

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