for f being FinSequence of (TOP-REAL 2)
for n being Element of NAT st 2 <= n & f is being_S-Seq holds
f | n is being_S-Seq