for X being non empty set
for seq being sequence of X
for f being FinSequence of X st rng f c= rng seq holds
ex N being Nat st rng f c= rng (seq | (Segm N))