theorem LM1: :: TOPMETR4:1

for M being non empty set
for x being sequence of M st rng x is finite holds
ex z being Element of M st
( x " {z} c= NAT & x " {z} is infinite )