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 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:27;
A4: 2 in dom f by A2, FINSEQ_3:27;
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:27;
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 by XBOOLE_0:4;

now

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 5;
1 + 1 = 2 ;
then f /. 1 in {(f /. 2)} by A1, A8, A10, A11, TOPREAL1:def 8;
then f /. 1 = f /. 2 by TARSKI:def 1;
hence contradiction by A1, A3, A4, PARTFUN2:17; :: thesis: verum

end;

suppose i > 2 ; :: thesis: contradiction

then 1 + 1 < i ;
hence contradiction by A1, A9, TOPREAL1:def 9; :: 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 5; :: thesis: verum

end;

end;