theorem Th7: :: LOPBAN_5:7

for X being RealBanachSpace
for X0 being Subset of (LinearTopSpaceNorm X)
for Y being RealBanachSpace
for vseq being sequence of (R_NormSpace_of_BoundedLinearOperators (X,Y)) st X0 is dense & ( for x being Point of X st x in X0 holds
vseq # x is convergent ) & ( for x being Point of X ex K being Real st
( 0 <= K & ( for n being Nat holds ||.((vseq # x) . n).|| <= K ) ) ) holds
for x being Point of X holds vseq # x is convergent