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;
1 <= j
by A2, A3, XXREAL_0:2;
then A7:
f /. j in LSeg f,j
by A6, TOPREAL1:27;
A8:
i < len f
by A3, A4, XXREAL_0:2;
then
i + 1 <= len f
by NAT_1:13;
then A9:
f /. i in LSeg f,i
by A2, TOPREAL1:27;
A10:
i + 1 <= j
by A3, NAT_1:13;
A11:
i <> 0
by A2;
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 A10, A11, NAT_1:27, XXREAL_0:1;
suppose that A12:
i + 1
= j
and A13:
i = 1
;
:: thesis: contradictionA14:
((len f) -' 1) + 1
= len f
by A1, XREAL_1:237, XXREAL_0:2;
1
+ 1
<= len f
by A1, XXREAL_0:2;
then A15:
1
<= (len f) -' 1
by A14, XREAL_1:8;
A16:
(len f) -' 1
< len f
by A14, XREAL_1:31;
(j + 1) + 1
< len f
by A1, A12, A13;
then
j + 1
< (len f) -' 1
by A14, XREAL_1:8;
then
LSeg f,
j misses LSeg f,
((len f) -' 1)
by A12, A13, A16, GOBOARD5:def 4;
then A17:
(LSeg f,j) /\ (LSeg f,((len f) -' 1)) = {}
by XBOOLE_0:def 7;
f /. i = f /. (len f)
by A13, FINSEQ_6:def 1;
then
f /. i in LSeg f,
((len f) -' 1)
by A14, A15, TOPREAL1:27;
hence
contradiction
by A5, A7, A17, XBOOLE_0:def 4;
:: thesis: verum end; suppose that A18:
i + 1
= j
and A19:
i = 1
+ 1
;
:: thesis: contradictionA20:
(i -' 1) + 1
= i
by A2, XREAL_1:237;
j + 1
< len f
by A1, A18, A19;
then
LSeg f,
(i -' 1) misses LSeg f,
j
by A3, A20, GOBOARD5:def 4;
then A21:
(LSeg f,(i -' 1)) /\ (LSeg f,j) = {}
by XBOOLE_0:def 7;
f /. i in LSeg f,
(i -' 1)
by A8, A19, A20, TOPREAL1:27;
hence
contradiction
by A5, A7, A21, XBOOLE_0:def 4;
:: thesis: verum end; suppose A22:
i > 1
+ 1
;
:: thesis: contradictionA23:
(i -' 1) + 1
= i
by A2, XREAL_1:237;
then A24:
1
< i -' 1
by A22, XREAL_1:8;
then
LSeg f,
(i -' 1) misses LSeg f,
j
by A3, A4, A23, GOBOARD5:def 4;
then A25:
(LSeg f,(i -' 1)) /\ (LSeg f,j) = {}
by XBOOLE_0:def 7;
f /. i in LSeg f,
(i -' 1)
by A8, A23, A24, TOPREAL1:27;
hence
contradiction
by A5, A7, A25, XBOOLE_0:def 4;
:: thesis: verum end; suppose that A26:
i + 1
< j
and A27:
i <> 1
;
:: thesis: contradiction
1
< i
by A2, A27, XXREAL_0:1;
then
LSeg f,
i misses LSeg f,
j
by A4, A26, GOBOARD5:def 4;
then
(LSeg f,i) /\ (LSeg f,j) = {}
by XBOOLE_0:def 7;
hence
contradiction
by A5, A7, A9, XBOOLE_0:def 4;
:: thesis: verum suppose that A28:
i + 1
< j
and A29:
j + 1
<> len f
;
:: thesis: contradiction
j + 1
< len f
by A6, A29, XXREAL_0:1;
then
LSeg f,
i misses LSeg f,
j
by A28, GOBOARD5:def 4;
then
(LSeg f,i) /\ (LSeg f,j) = {}
by XBOOLE_0:def 7;
hence
contradiction
by A5, A7, A9, XBOOLE_0:def 4;
:: thesis: verum end; suppose that A30:
i + 1
< j
and A31:
i = 1
and A32:
j + 1
= len f
;
:: thesis: contradictionA33:
(j -' 1) + 1
= j
by A2, A3, XREAL_1:237, XXREAL_0:2;
then A34:
i + 1
<= j -' 1
by A30, NAT_1:13;
i + 1
<> j -' 1
by A1, A31, A32, A33;
then A35:
i + 1
< j -' 1
by A34, XXREAL_0:1;
1
<= j -' 1
by A31, A34, XXREAL_0:2;
then A36:
f /. j in LSeg f,
(j -' 1)
by A4, A33, TOPREAL1:27;
j < len f
by A32, NAT_1:13;
then
LSeg f,1
misses LSeg f,
(j -' 1)
by A31, A33, A35, GOBOARD5:def 4;
then
(LSeg f,1) /\ (LSeg f,(j -' 1)) = {}
by XBOOLE_0:def 7;
hence
contradiction
by A5, A9, A31, A36, XBOOLE_0:def 4;
:: thesis: verum end;