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

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