theorem Th15: :: NORMSP_4:12

for X being RealLinearSpace
for x being sequence of X
for A being finite Subset of X st A c= rng x holds
ex n being Nat st A c= rng (x | (Segm n))