let f be non constant standard clockwise_oriented special_circular_sequence; :: thesis:
let G be Go-board; :: thesis:
let k be Element of NAT ; :: thesis:
assume that
A1: f is_sequence_on G and
A2: ( 1 <= k & k + 1 <= len f ) and
A3: f /. k = N-min (L~ f) ; :: thesis:
consider i1, j1, i2, j2 being Element of NAT such that
A4: [i1,j1] in Indices G and
A5: f /. k = G * i1,j1 and
A6: [i2,j2] in Indices G and
A7: f /. (k + 1) = G * i2,j2 and
A8: ( ( i1 = i2 & j1 + 1 = j2 ) or ( i1 + 1 = i2 & j1 = j2 ) or ( i1 = i2 + 1 & j1 = j2 ) or ( i1 = i2 & j1 = j2 + 1 ) ) by A1, A2, JORDAN8:6;
A9: ( 1 <= i1 & i1 <= len G & 1 <= j1 & j1 <= width G ) by A4, MATRIX_1:39;
A10: ( 1 <= i2 & i2 <= len G & 1 <= j2 & j2 <= width G ) by A6, MATRIX_1:39;
A11: (G * i1,j1) `2 = N-bound (L~ f) by A3, A5, EUCLID:56;
A12: k + 1 >= 1 + 1 by A2, XREAL_1:9;
then A13: len f >= 2 by A2, XXREAL_0:2;
k + 1 >= 1 by NAT_1:11;
then A14: k + 1 in dom f by A2, FINSEQ_3:27;
then f /. (k + 1) in L~ f by A2, A12, GOBOARD1:16, XXREAL_0:2;
then A15: (G * i1,j1) `2 >= (G * i2,j2) `2 by A7, A11, PSCOMP_1:71;
reconsider f1 = f as non trivial FinSequence of (TOP-REAL 2) ;
take i1 ; :: thesis:
take j1 ; :: thesis:
A16: k < len f by A2, NAT_1:13;
then A17: k in dom f by A2, FINSEQ_3:27;

per cases by A8;

suppose A18: ( i1 + 1 = i2 & j1 = j2 ) ; :: thesis:

thus [i1,j1] in Indices G by A4; :: thesis:
thus [(i1 + 1),j1] in Indices G by A6, A18; :: thesis:
thus f /. k = G * i1,j1 by A5; :: thesis:
thus f /. (k + 1) = G * (i1 + 1),j1 by A7, A18; :: thesis:

end;

suppose A19: ( i1 = i2 & j2 + 1 = j1 & k <> 1 ) ; :: thesis:

reconsider k' = k - 1 as Element of NAT by A17, FINSEQ_3:28;
k > 1 by A2, A19, XXREAL_0:1;
then k >= 1 + 1 by NAT_1:13;
then A20: k' >= (1 + 1) - 1 by XREAL_1:11;
A21: k' + 1 < len f by A2, NAT_1:13;
consider i3, j3, i4, j4 being Element of NAT such that
A22: [i3,j3] in Indices G and
A23: f /. k' = G * i3,j3 and
A24: [i4,j4] in Indices G and
A25: f /. (k' + 1) = G * i4,j4 and
A26: ( ( i3 = i4 & j3 + 1 = j4 ) or ( i3 + 1 = i4 & j3 = j4 ) or ( i3 = i4 + 1 & j3 = j4 ) or ( i3 = i4 & j3 = j4 + 1 ) ) by A1, A16, A20, JORDAN8:6;
A27: k' + 1 = k ;
A28: ( i1 = i4 & j1 = j4 ) by A4, A5, A24, A25, GOBOARD1:21;
A29: ( 1 <= i3 & i3 <= len G & 1 <= j3 & j3 <= width G ) by A22, MATRIX_1:39;
k' < len f by A21, NAT_1:13;
then A30: k' in dom f by A20, FINSEQ_3:27;
then f /. k' in L~ f by A2, A12, GOBOARD1:16, XXREAL_0:2;
then A31: (G * i1,j1) `2 >= (G * i3,j3) `2 by A11, A23, PSCOMP_1:71;
A32: i3 = i4

proof

assume A33: i3 <> i4 ; :: thesis:

per cases by A26, A33;

suppose A34: ( j3 = j4 & i3 = i4 + 1 ) ; :: thesis:

then (G * i3,j3) `2 <> N-bound (L~ f) by A1, A16, A20, A22, A23, A24, A25, Th19;
then (G * 1,j3) `2 <> N-bound (L~ f) by A29, GOBOARD5:2;
then (N-min (L~ f)) `2 <> N-bound (L~ f) by A3, A5, A9, A28, A34, GOBOARD5:2;
hence contradiction by EUCLID:56; :: thesis:

end;

suppose A35: ( j3 = j4 & i3 + 1 = i4 ) ; :: thesis:

(G * i3,j3) `2 = (G * 1,j3) `2 by A29, GOBOARD5:2
.= (N-min (L~ f)) `2 by A3, A5, A9, A28, A35, GOBOARD5:2
.= N-bound (L~ f) by EUCLID:56 ;
then ( G * i3,j3 in N-most (L~ f) & L~ f = L~ f1 ) by A13, A23, A30, GOBOARD1:16, SPRECT_2:14;
then (G * i4,j4) `1 <= (G * i3,j3) `1 by A3, A25, PSCOMP_1:98;
then i3 >= i3 + 1 by A9, A28, A29, A35, GOBOARD5:4;
hence contradiction by NAT_1:13; :: thesis:

end;

now

per cases by A26, A32;

suppose j4 + 1 = j3 ; :: thesis:

then j4 >= j4 + 1 by A9, A28, A29, A31, A32, GOBOARD5:5;
hence contradiction by NAT_1:13; :: thesis:

end;

suppose A36: j4 = j3 + 1 ; :: thesis:

k' + (1 + 1) <= len f by A2;
then A37: (LSeg f,k') /\ (LSeg f,k) = {(f /. k)} by A20, A27, TOPREAL1:def 8;
A38: j1 <> j2 by A19;
( f /. k' in LSeg f,k' & f /. (k + 1) in LSeg f,k ) by A2, A16, A20, A27, TOPREAL1:27;
then f /. (k + 1) in {(f /. k)} by A7, A19, A23, A28, A32, A36, A37, XBOOLE_0:def 4;
then f /. (k + 1) = f /. k by TARSKI:def 1;
hence contradiction by A4, A5, A6, A7, A38, GOBOARD1:21; :: thesis:

end;

hence ( [i1,j1] in Indices G & [(i1 + 1),j1] in Indices G & f /. k = G * i1,j1 & f /. (k + 1) = G * (i1 + 1),j1 ) ; :: thesis:

end;

suppose A39: ( i1 = i2 & j2 + 1 = j1 & k = 1 ) ; :: thesis:

set k1 = len f;
A40: f /. (len f) = f /. 1 by FINSEQ_6:def 1;
k < len f by A2, NAT_1:13;
then A41: len f > 1 + 0 by A2, XXREAL_0:2;
then len f in dom f by FINSEQ_3:27;
then reconsider k' = (len f) - 1 as Element of NAT by FINSEQ_3:28;
k + 1 >= 1 + 1 by A2, XREAL_1:9;
then len f >= 1 + 1 by A2, XXREAL_0:2;
then A42: k' >= (1 + 1) - 1 by XREAL_1:11;
A43: k' + 1 <= len f ;
consider i3, j3, i4, j4 being Element of NAT such that
A44: [i3,j3] in Indices G and
A45: f /. k' = G * i3,j3 and
A46: [i4,j4] in Indices G and
A47: f /. (k' + 1) = G * i4,j4 and
A48: ( ( i3 = i4 & j3 + 1 = j4 ) or ( i3 + 1 = i4 & j3 = j4 ) or ( i3 = i4 + 1 & j3 = j4 ) or ( i3 = i4 & j3 = j4 + 1 ) ) by A1, A42, JORDAN8:6;
A49: k' + 1 = len f ;
A50: ( i1 = i4 & j1 = j4 ) by A4, A5, A39, A40, A46, A47, GOBOARD1:21;
A51: ( 1 <= i3 & i3 <= len G & 1 <= j3 & j3 <= width G ) by A44, MATRIX_1:39;
k' < len f by A43, NAT_1:13;
then A52: k' in dom f by A42, FINSEQ_3:27;
then f /. k' in L~ f by A2, A12, GOBOARD1:16, XXREAL_0:2;
then A53: (G * i1,j1) `2 >= (G * i3,j3) `2 by A11, A45, PSCOMP_1:71;
A54: i3 = i4

proof

assume A55: i3 <> i4 ; :: thesis:

per cases by A48, A55;

suppose A56: ( j3 = j4 & i3 = i4 + 1 ) ; :: thesis:

then (G * i3,j3) `2 <> N-bound (L~ f) by A1, A42, A44, A45, A46, A47, Th19;
then (G * 1,j3) `2 <> N-bound (L~ f) by A51, GOBOARD5:2;
then (N-min (L~ f)) `2 <> N-bound (L~ f) by A3, A5, A9, A50, A56, GOBOARD5:2;
hence contradiction by EUCLID:56; :: thesis:

end;

suppose A57: ( j3 = j4 & i3 + 1 = i4 ) ; :: thesis:

(G * i3,j3) `2 = (G * 1,j3) `2 by A51, GOBOARD5:2
.= (N-min (L~ f)) `2 by A3, A5, A9, A50, A57, GOBOARD5:2
.= N-bound (L~ f) by EUCLID:56 ;
then ( G * i3,j3 in N-most (L~ f) & L~ f = L~ f1 ) by A13, A45, A52, GOBOARD1:16, SPRECT_2:14;
then (G * i4,j4) `1 <= (G * i3,j3) `1 by A3, A39, A40, A47, PSCOMP_1:98;
then i3 >= i3 + 1 by A9, A50, A51, A57, GOBOARD5:4;
hence contradiction by NAT_1:13; :: thesis:

end;

now

per cases by A48, A54;

suppose j4 + 1 = j3 ; :: thesis:

then j4 >= j4 + 1 by A9, A50, A51, A53, A54, GOBOARD5:5;
hence contradiction by NAT_1:13; :: thesis:

end;

suppose A58: j4 = j3 + 1 ; :: thesis:

(len f) - 1 >= 0 by A41, XREAL_1:21;
then (len f) -' 1 = (len f) - 1 by XREAL_0:def 2;
then A59: (LSeg f,k) /\ (LSeg f,k') = {(f . k)} by A39, JORDAN4:54
.= {(f /. k)} by A17, PARTFUN1:def 8 ;
A60: j1 <> j2 by A39;
( f /. k' in LSeg f,k' & f /. (k + 1) in LSeg f,k ) by A2, A42, A49, TOPREAL1:27;
then f /. (k + 1) in {(f /. k)} by A7, A39, A45, A50, A54, A58, A59, XBOOLE_0:def 4;
then f /. (k + 1) = f /. k by TARSKI:def 1;
hence contradiction by A4, A5, A6, A7, A60, GOBOARD1:21; :: thesis:

end;

hence ( [i1,j1] in Indices G & [(i1 + 1),j1] in Indices G & f /. k = G * i1,j1 & f /. (k + 1) = G * (i1 + 1),j1 ) ; :: thesis:

end;

suppose ( i1 = i2 & j2 = j1 + 1 ) ; :: thesis:

then j1 >= j1 + 1 by A9, A10, A15, GOBOARD5:5;
hence ( [i1,j1] in Indices G & [(i1 + 1),j1] in Indices G & f /. k = G * i1,j1 & f /. (k + 1) = G * (i1 + 1),j1 ) by NAT_1:13; :: thesis:

end;

suppose A61: ( i1 = i2 + 1 & j1 = j2 ) ; :: thesis:

(G * i2,j2) `2 = (G * 1,j2) `2 by A10, GOBOARD5:2
.= N-bound (L~ f) by A9, A11, A61, GOBOARD5:2 ;
then ( G * i2,j2 in N-most (L~ f) & L~ f = L~ f1 ) by A7, A13, A14, GOBOARD1:16, SPRECT_2:14;
then (G * i1,j1) `1 <= (G * i2,j2) `1 by A3, A5, PSCOMP_1:98;
then i2 >= i2 + 1 by A9, A10, A61, GOBOARD5:4;
hence ( [i1,j1] in Indices G & [(i1 + 1),j1] in Indices G & f /. k = G * i1,j1 & f /. (k + 1) = G * (i1 + 1),j1 ) by NAT_1:13; :: thesis:

end;