for X being RealNormSpace-Sequence
for Y being RealNormSpace st Y is complete holds
for seq being sequence of (R_NormSpace_of_BoundedMultilinearOperators (X,Y)) st seq is Cauchy_sequence_by_Norm holds
seq is convergent