theorem Th7: :: LOPBAN_3:7

for X being RealNormSpace
for seq, seq1 being sequence of X st seq1 is subsequence of seq & seq is convergent holds
seq1 is convergent