let f be FinSequence of (TOP-REAL 2); :: thesis:
let i be Nat; :: thesis:
assume that
A1: ( f is unfolded & f is s.n.c. & f is one-to-one ) and
A2: 2 <= len f ; :: thesis:
1 <= len f by A2, XXREAL_0:2;
then A3: 1 in dom f by FINSEQ_3:25;
A4: 2 in dom f by A2, FINSEQ_3:25;
assume A5: f /. 1 in LSeg (f,i) ; :: thesis:
assume A6: i <> 1 ; :: thesis:

per cases by A6, XXREAL_0:1;

suppose A7: i > 1 ; :: thesis:

1 + 1 <= len f by A2;
then f /. 1 in LSeg (f,1) by TOPREAL1:21;
then A8: f /. 1 in (LSeg (f,1)) /\ (LSeg (f,i)) by A5, XBOOLE_0:def 4;
then A9: LSeg (f,1) meets LSeg (f,i) ;

now :: thesis:

per cases by XXREAL_0:1;

suppose A10: i = 2 ; :: thesis:

then A11: 1 + 2 <= len f by A5, TOPREAL1:def 3;
1 + 1 = 2 ;
then f /. 1 in {(f /. 2)} by A1, A8, A10, A11, TOPREAL1:def 6;
then f /. 1 = f /. 2 by TARSKI:def 1;
hence contradiction by A1, A3, A4, PARTFUN2:10; :: thesis:

end;

suppose i > 2 ; :: thesis:

then 1 + 1 < i ;
hence contradiction by A1, A9, TOPREAL1:def 7; :: thesis:

end;

suppose i < 2 ; :: thesis:

then i < 1 + 1 ;
hence contradiction by A7, NAT_1:13; :: thesis:

end;

end;

end;

hence contradiction ; :: thesis:

end;

suppose i < 1 ; :: thesis:

hence contradiction by A5, TOPREAL1:def 3; :: thesis:

end;

end;