let f be circular s.c.c. FinSequence of (TOP-REAL 2); :: thesis: ( len f > 4 implies for i, j being Nat st 1 <= i & i < j & j < len f holds

f /. i <> f /. j )

assume A1: len f > 4 ; :: thesis: for i, j being Nat st 1 <= i & i < j & j < len f holds

f /. i <> f /. j

let i, j be 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:21;

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:21;

( i <= 2 implies not not i = 0 & ... & not i = 2 ) ;

f /. i <> f /. j )

assume A1: len f > 4 ; :: thesis: for i, j being Nat st 1 <= i & i < j & j < len f holds

f /. i <> f /. j

let i, j be 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:21;

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:21;

( i <= 2 implies not not i = 0 & ... & not i = 2 ) ;

per cases then
( ( 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, XXREAL_0:1;

end;

suppose that A11:
i + 1 = j
and

A12: i = 1 ; :: thesis: contradiction

A12: i = 1 ; :: thesis: contradiction

A13:
((len f) -' 1) + 1 = len f
by A1, XREAL_1:235, XXREAL_0:2;

(j + 1) + 1 < len f by A1, A11, A12;

then A14: j + 1 < (len f) -' 1 by A13, XREAL_1:6;

(len f) -' 1 < len f by A13, XREAL_1:29;

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:6;

then f /. i in LSeg (f,((len f) -' 1)) by A13, A16, TOPREAL1:21;

hence contradiction by A5, A8, A15, XBOOLE_0:def 4; :: thesis: verum

end;(j + 1) + 1 < len f by A1, A11, A12;

then A14: j + 1 < (len f) -' 1 by A13, XREAL_1:6;

(len f) -' 1 < len f by A13, XREAL_1:29;

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:6;

then f /. i in LSeg (f,((len f) -' 1)) by A13, A16, TOPREAL1:21;

hence contradiction by A5, A8, A15, XBOOLE_0:def 4; :: thesis: verum

suppose that A17:
i + 1 = j
and

A18: i = 1 + 1 ; :: thesis: contradiction

A18: i = 1 + 1 ; :: thesis: contradiction

A19:
(i -' 1) + 1 = i
by A2, XREAL_1:235;

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:21;

hence contradiction by A5, A8, A20, XBOOLE_0:def 4; :: thesis: verum

end;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:21;

hence contradiction by A5, A8, A20, XBOOLE_0:def 4; :: thesis: verum

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

A22:
(i -' 1) + 1 = i
by A2, XREAL_1:235;

then A23: 1 < i -' 1 by A21, XREAL_1:6;

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:21;

hence contradiction by A5, A8, A24, XBOOLE_0:def 4; :: thesis: verum

end;then A23: 1 < i -' 1 by A21, XREAL_1:6;

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:21;

hence contradiction by A5, A8, A24, XBOOLE_0:def 4; :: thesis: verum

suppose that A25:
i + 1 < j
and

A26: i <> 1 ; :: thesis: contradiction

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;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

suppose that A27:
i + 1 < j
and

A28: j + 1 <> len f ; :: thesis: contradiction

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;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

suppose that A29:
i + 1 < j
and

A30: i = 1 and

A31: j + 1 = len f ; :: thesis: contradiction

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:235, 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:21;

hence contradiction by A5, A10, A30, A35, XBOOLE_0:def 4; :: thesis: verum

end;A33: (j -' 1) + 1 = j by A2, A3, XREAL_1:235, 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:21;

hence contradiction by A5, A10, A30, A35, XBOOLE_0:def 4; :: thesis: verum