let X, Y be RealNormSpace; :: thesis: for Z being RealBanachSpace holds R_NormSpace_of_BoundedBilinearOperators (X,Y,Z) is RealBanachSpace

let Z be RealBanachSpace; :: thesis: R_NormSpace_of_BoundedBilinearOperators (X,Y,Z) is RealBanachSpace

for seq being sequence of (R_NormSpace_of_BoundedBilinearOperators (X,Y,Z)) st seq is Cauchy_sequence_by_Norm holds

seq is convergent by Th42;

hence R_NormSpace_of_BoundedBilinearOperators (X,Y,Z) is RealBanachSpace by LOPBAN_1:def 15; :: thesis: verum

let Z be RealBanachSpace; :: thesis: R_NormSpace_of_BoundedBilinearOperators (X,Y,Z) is RealBanachSpace

for seq being sequence of (R_NormSpace_of_BoundedBilinearOperators (X,Y,Z)) st seq is Cauchy_sequence_by_Norm holds

seq is convergent by Th42;

hence R_NormSpace_of_BoundedBilinearOperators (X,Y,Z) is RealBanachSpace by LOPBAN_1:def 15; :: thesis: verum