theorem Th5: :: NFCONT_1:5

for n being Nat
for S, T being RealNormSpace
for seq being sequence of S
for h being PartFunc of S,T st rng seq c= dom h holds
seq . n in dom h