let X be ComplexNormSpace; :: thesis: for Y being ComplexBanachSpace holds C_NormSpace_of_BoundedLinearOperators (X,Y) is ComplexBanachSpace
let Y be ComplexBanachSpace; :: thesis: C_NormSpace_of_BoundedLinearOperators (X,Y) is ComplexBanachSpace
for seq being sequence of (C_NormSpace_of_BoundedLinearOperators (X,Y)) st seq is Cauchy_sequence_by_Norm holds
seq is convergent by Th41;
hence C_NormSpace_of_BoundedLinearOperators (X,Y) is ComplexBanachSpace by Def13; :: thesis: verum