let f be FinSequence of (TOP-REAL 2); :: thesis: for i being Element of 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 Element of 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 A1: ( f is unfolded & f is s.n.c. & f is one-to-one & 2 <= len f ) ; :: thesis: ( not f /. 1 in LSeg f,i or i = 1 )
then 1 <= len f by XXREAL_0:2;
then A2: ( 1 in dom f & 2 in dom f ) by A1, FINSEQ_3:27;
assume A3: f /. 1 in LSeg f,i ; :: thesis: i = 1
assume A4: i <> 1 ; :: thesis: contradiction

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

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

1 + 1 <= len f by A1;
then f /. 1 in LSeg f,1 by TOPREAL1:27;
then A6: f /. 1 in (LSeg f,1) /\ (LSeg f,i) by A3, XBOOLE_0:def 4;
then A7: LSeg f,1 meets LSeg f,i by XBOOLE_0:4;

now

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

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

then A9: 1 + 2 <= len f by A3, TOPREAL1:def 5;
1 + 1 = 2 ;
then f /. 1 in {(f /. 2)} by A1, A6, A8, A9, TOPREAL1:def 8;
then f /. 1 = f /. 2 by TARSKI:def 1;
hence contradiction by A1, A2, PARTFUN2:17; :: thesis: verum

end;

suppose i > 2 ; :: thesis: contradiction

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

end;

suppose i < 2 ; :: thesis: contradiction

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

end;

end;

end;

hence contradiction ; :: thesis: verum

end;

suppose i < 1 ; :: thesis: contradiction

hence contradiction by A3, TOPREAL1:def 5; :: thesis: verum

end;

end;