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