theorem :: TOPREAL3:33
for f being FinSequence of (TOP-REAL 2)
for i being Nat st i > 2 & i in dom f & f is being_S-Seq holds
f | i is being_S-Seq