let f be circular s.c.c. FinSequence of (TOP-REAL 2); :: thesis: ( len f > 4 implies for i, j being Element of NAT st 1 <= i & i < j & j < len f holds
f /. i <> f /. j )
assume A1: len f > 4 ; :: thesis: for i, j being Element of NAT st 1 <= i & i < j & j < len f holds
f /. i <> f /. j
let i, j be Element of NAT ; :: thesis: ( 1 <= i & i < j & j < len f implies f /. i <> f /. j )
assume that
A2: 1 <= i and
A3: i < j and
A4: j < len f and
A5: f /. i = f /. j ; :: thesis: contradiction
A6: j + 1 <= len f by A4, NAT_1:13;
A7: ( i + 1 <= j & i <> 0 ) by A2, A3, NAT_1:13;
1 <= j by A2, A3, XXREAL_0:2;
then A8: f /. j in LSeg f,j by A6, TOPREAL1:27;
A9: i < len f by A3, A4, XXREAL_0:2;
then i + 1 <= len f by NAT_1:13;
then A10: f /. i in LSeg f,i by A2, TOPREAL1:27;

per cases ( ( i + 1 = j & i = 1 ) or ( i + 1 = j & i = 1 + 1 ) or i > 1 + 1 or ( i + 1 < j & i <> 1 ) or ( i + 1 < j & j + 1 <> len f ) or ( i + 1 < j & i = 1 & j + 1 = len f ) ) by A7, NAT_1:27, XXREAL_0:1;

suppose that A11: i + 1 = j and
A12: i = 1 ; :: thesis: contradiction

A13: ((len f) -' 1) + 1 = len f by A1, XREAL_1:237, XXREAL_0:2;
(j + 1) + 1 < len f by A1, A11, A12;
then A14: j + 1 < (len f) -' 1 by A13, XREAL_1:8;
(len f) -' 1 < len f by A13, XREAL_1:31;
then LSeg f,j misses LSeg f,((len f) -' 1) by A11, A12, A14, GOBOARD5:def 4;
then A15: (LSeg f,j) /\ (LSeg f,((len f) -' 1)) = {} by XBOOLE_0:def 7;
A16: f /. i = f /. (len f) by A12, FINSEQ_6:def 1;
1 + 1 <= len f by A1, XXREAL_0:2;
then 1 <= (len f) -' 1 by A13, XREAL_1:8;
then f /. i in LSeg f,((len f) -' 1) by A13, A16, TOPREAL1:27;
hence contradiction by A5, A8, A15, XBOOLE_0:def 4; :: thesis: verum

end;

suppose that A17: i + 1 = j and
A18: i = 1 + 1 ; :: thesis: contradiction

A19: (i -' 1) + 1 = i by A2, XREAL_1:237;
j + 1 < len f by A1, A17, A18;
then LSeg f,(i -' 1) misses LSeg f,j by A3, A19, GOBOARD5:def 4;
then A20: (LSeg f,(i -' 1)) /\ (LSeg f,j) = {} by XBOOLE_0:def 7;
f /. i in LSeg f,(i -' 1) by A9, A18, A19, TOPREAL1:27;
hence contradiction by A5, A8, A20, XBOOLE_0:def 4; :: thesis: verum

end;

suppose A21: i > 1 + 1 ; :: thesis: contradiction

A22: (i -' 1) + 1 = i by A2, XREAL_1:237;
then A23: 1 < i -' 1 by A21, XREAL_1:8;
then LSeg f,(i -' 1) misses LSeg f,j by A3, A4, A22, GOBOARD5:def 4;
then A24: (LSeg f,(i -' 1)) /\ (LSeg f,j) = {} by XBOOLE_0:def 7;
f /. i in LSeg f,(i -' 1) by A9, A22, A23, TOPREAL1:27;
hence contradiction by A5, A8, A24, XBOOLE_0:def 4; :: thesis: verum

end;

suppose that A25: i + 1 < j and
A26: i <> 1 ; :: thesis: contradiction

1 < i by A2, A26, XXREAL_0:1;
then LSeg f,i misses LSeg f,j by A4, A25, GOBOARD5:def 4;
then (LSeg f,i) /\ (LSeg f,j) = {} by XBOOLE_0:def 7;
hence contradiction by A5, A8, A10, XBOOLE_0:def 4; :: thesis: verum

end;

suppose that A27: i + 1 < j and
A28: j + 1 <> len f ; :: thesis: contradiction

j + 1 < len f by A6, A28, XXREAL_0:1;
then LSeg f,i misses LSeg f,j by A27, GOBOARD5:def 4;
then (LSeg f,i) /\ (LSeg f,j) = {} by XBOOLE_0:def 7;
hence contradiction by A5, A8, A10, XBOOLE_0:def 4; :: thesis: verum

end;

suppose that A29: i + 1 < j and
A30: i = 1 and
A31: j + 1 = len f ; :: thesis: contradiction

A32: j < len f by A31, NAT_1:13;
A33: (j -' 1) + 1 = j by A2, A3, XREAL_1:237, XXREAL_0:2;
then A34: i + 1 <= j -' 1 by A29, NAT_1:13;
i + 1 <> j -' 1 by A1, A30, A31, A33;
then i + 1 < j -' 1 by A34, XXREAL_0:1;
then LSeg f,1 misses LSeg f,(j -' 1) by A30, A33, A32, GOBOARD5:def 4;
then A35: (LSeg f,1) /\ (LSeg f,(j -' 1)) = {} by XBOOLE_0:def 7;
1 <= j -' 1 by A30, A34, XXREAL_0:2;
then f /. j in LSeg f,(j -' 1) by A4, A33, TOPREAL1:27;
hence contradiction by A5, A10, A30, A35, XBOOLE_0:def 4; :: thesis: verum

end;

end;