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 CCauchy holds
seq is convergent by Th46;
hence C_NormSpace_of_BoundedLinearOperators X,Y is ComplexBanachSpace by Def14; :: thesis: verum