for f being FinSequence of (TOP-REAL 2)
for i being Nat st f is unfolded & f is s.n.c. & f is one-to-one & f /. (len f) in LSeg (f,i) & i in dom f & i + 1 in dom f holds
i + 1 = len f