let X be RealNormSpace; :: thesis: for Y being RealBanachSpace holds R_NormSpace_of_BoundedLinearOperators (X,Y) is RealBanachSpace
let Y be RealBanachSpace; :: thesis: R_NormSpace_of_BoundedLinearOperators (X,Y) is RealBanachSpace
for seq being sequence of (R_NormSpace_of_BoundedLinearOperators (X,Y)) st seq is Cauchy_sequence_by_Norm holds
seq is convergent by Th42;
hence R_NormSpace_of_BoundedLinearOperators (X,Y) is RealBanachSpace by Def15; :: thesis: verum