let f be FinSequence of (TOP-REAL 2); :: thesis: for i being Nat st f is unfolded & f is s.n.c. & f is one-to-one & len f >= 2 & f /. 1 in LSeg (f,i) holds
i = 1
let i be Nat; :: thesis: ( f is unfolded & f is s.n.c. & f is one-to-one & len f >= 2 & f /. 1 in LSeg (f,i) implies i = 1 )
assume that
A1: ( f is unfolded & f is s.n.c. & f is one-to-one ) and
A2: 2 <= len f ; :: thesis: ( not f /. 1 in LSeg (f,i) or i = 1 )
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: i = 1
assume A6: i <> 1 ; :: thesis: contradiction

per cases ( i > 1 or i < 1 ) by A6, XXREAL_0:1;

suppose A7: i > 1 ; :: thesis: contradiction

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: contradiction

per cases ( i = 2 or i > 2 or i < 2 ) by XXREAL_0:1;

suppose A10: i = 2 ; :: thesis: contradiction

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: verum

end;

suppose i > 2 ; :: thesis: contradiction

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

end;

suppose i < 2 ; :: thesis: contradiction

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

end;

end;

end;

hence contradiction ; :: thesis: verum

end;

suppose i < 1 ; :: thesis: contradiction

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

end;

end;