let f be circular s.c.c. FinSequence of (TOP-REAL 2); ( 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
; for i, j being Nat st 1 <= i & i < j & j < len f holds
f /. i <> f /. j
let i, j be Nat; ( 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
; 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;
suppose that A11:
i + 1
= j
and A12:
i = 1
;
contradictionA13:
((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;
verum end; suppose that A17:
i + 1
= j
and A18:
i = 1
+ 1
;
contradictionA19:
(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;
verum end; suppose A21:
i > 1
+ 1
;
contradictionA22:
(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;
verum end; suppose that A25:
i + 1
< j
and A26:
i <> 1
;
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;
verum suppose that A27:
i + 1
< j
and A28:
j + 1
<> len f
;
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;
verum end; suppose that A29:
i + 1
< j
and A30:
i = 1
and A31:
j + 1
= len f
;
contradictionA32:
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;
verum end;