let f be V22() standard clockwise_oriented special_circular_sequence; :: thesis: for G being Go-board

for k being Nat st f is_sequence_on G & 1 <= k & k + 1 <= len f & f /. k = N-min (L~ f) holds

ex i, j being Nat st

( [i,j] in Indices G & [(i + 1),j] in Indices G & f /. k = G * (i,j) & f /. (k + 1) = G * ((i + 1),j) )

let G be Go-board; :: thesis: for k being Nat st f is_sequence_on G & 1 <= k & k + 1 <= len f & f /. k = N-min (L~ f) holds

ex i, j being Nat st

( [i,j] in Indices G & [(i + 1),j] in Indices G & f /. k = G * (i,j) & f /. (k + 1) = G * ((i + 1),j) )

let k be Nat; :: thesis: ( f is_sequence_on G & 1 <= k & k + 1 <= len f & f /. k = N-min (L~ f) implies ex i, j being Nat st

( [i,j] in Indices G & [(i + 1),j] in Indices G & f /. k = G * (i,j) & f /. (k + 1) = G * ((i + 1),j) ) )

assume that

A1: f is_sequence_on G and

A2: 1 <= k and

A3: k + 1 <= len f and

A4: f /. k = N-min (L~ f) ; :: thesis: ex i, j being Nat st

( [i,j] in Indices G & [(i + 1),j] in Indices G & f /. k = G * (i,j) & f /. (k + 1) = G * ((i + 1),j) )

consider i1, j1, i2, j2 being Nat such that

A5: [i1,j1] in Indices G and

A6: f /. k = G * (i1,j1) and

A7: [i2,j2] in Indices G and

A8: f /. (k + 1) = G * (i2,j2) and

A9: ( ( 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, A3, JORDAN8:3;

A10: (G * (i1,j1)) `2 = N-bound (L~ f) by A4, A6, EUCLID:52;

A11: j2 <= width G by A7, MATRIX_0:32;

A12: 1 <= i2 by A7, MATRIX_0:32;

take i1 ; :: thesis: ex j being Nat st

( [i1,j] in Indices G & [(i1 + 1),j] in Indices G & f /. k = G * (i1,j) & f /. (k + 1) = G * ((i1 + 1),j) )

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

A13: 1 <= i1 by A5, MATRIX_0:32;

A14: k + 1 >= 1 + 1 by A2, XREAL_1:7;

then A15: len f >= 2 by A3, XXREAL_0:2;

k + 1 >= 1 by NAT_1:11;

then A16: k + 1 in dom f by A3, FINSEQ_3:25;

then f /. (k + 1) in L~ f by A3, A14, GOBOARD1:1, XXREAL_0:2;

then A17: (G * (i1,j1)) `2 >= (G * (i2,j2)) `2 by A8, A10, PSCOMP_1:24;

A18: j1 <= width G by A5, MATRIX_0:32;

A19: k < len f by A3, NAT_1:13;

then A20: k in dom f by A2, FINSEQ_3:25;

A21: ( i2 <= len G & 1 <= j2 ) by A7, MATRIX_0:32;

A22: ( i1 <= len G & 1 <= j1 ) by A5, MATRIX_0:32;

for k being Nat st f is_sequence_on G & 1 <= k & k + 1 <= len f & f /. k = N-min (L~ f) holds

ex i, j being Nat st

( [i,j] in Indices G & [(i + 1),j] in Indices G & f /. k = G * (i,j) & f /. (k + 1) = G * ((i + 1),j) )

let G be Go-board; :: thesis: for k being Nat st f is_sequence_on G & 1 <= k & k + 1 <= len f & f /. k = N-min (L~ f) holds

ex i, j being Nat st

( [i,j] in Indices G & [(i + 1),j] in Indices G & f /. k = G * (i,j) & f /. (k + 1) = G * ((i + 1),j) )

let k be Nat; :: thesis: ( f is_sequence_on G & 1 <= k & k + 1 <= len f & f /. k = N-min (L~ f) implies ex i, j being Nat st

( [i,j] in Indices G & [(i + 1),j] in Indices G & f /. k = G * (i,j) & f /. (k + 1) = G * ((i + 1),j) ) )

assume that

A1: f is_sequence_on G and

A2: 1 <= k and

A3: k + 1 <= len f and

A4: f /. k = N-min (L~ f) ; :: thesis: ex i, j being Nat st

( [i,j] in Indices G & [(i + 1),j] in Indices G & f /. k = G * (i,j) & f /. (k + 1) = G * ((i + 1),j) )

consider i1, j1, i2, j2 being Nat such that

A5: [i1,j1] in Indices G and

A6: f /. k = G * (i1,j1) and

A7: [i2,j2] in Indices G and

A8: f /. (k + 1) = G * (i2,j2) and

A9: ( ( 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, A3, JORDAN8:3;

A10: (G * (i1,j1)) `2 = N-bound (L~ f) by A4, A6, EUCLID:52;

A11: j2 <= width G by A7, MATRIX_0:32;

A12: 1 <= i2 by A7, MATRIX_0:32;

take i1 ; :: thesis: ex j being Nat st

( [i1,j] in Indices G & [(i1 + 1),j] in Indices G & f /. k = G * (i1,j) & f /. (k + 1) = G * ((i1 + 1),j) )

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

A13: 1 <= i1 by A5, MATRIX_0:32;

A14: k + 1 >= 1 + 1 by A2, XREAL_1:7;

then A15: len f >= 2 by A3, XXREAL_0:2;

k + 1 >= 1 by NAT_1:11;

then A16: k + 1 in dom f by A3, FINSEQ_3:25;

then f /. (k + 1) in L~ f by A3, A14, GOBOARD1:1, XXREAL_0:2;

then A17: (G * (i1,j1)) `2 >= (G * (i2,j2)) `2 by A8, A10, PSCOMP_1:24;

A18: j1 <= width G by A5, MATRIX_0:32;

A19: k < len f by A3, NAT_1:13;

then A20: k in dom f by A2, FINSEQ_3:25;

A21: ( i2 <= len G & 1 <= j2 ) by A7, MATRIX_0:32;

A22: ( i1 <= len G & 1 <= j1 ) by A5, MATRIX_0:32;

per cases
( ( i1 + 1 = i2 & j1 = j2 ) or ( i1 = i2 & j2 + 1 = j1 & k <> 1 ) or ( i1 = i2 & j2 + 1 = j1 & k = 1 ) or ( i1 = i2 & j2 = j1 + 1 ) or ( i1 = i2 + 1 & j1 = j2 ) )
by A9;

end;

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

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

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

thus f /. k = G * (i1,j1) by A6; :: thesis: f /. (k + 1) = G * ((i1 + 1),j1)

thus f /. (k + 1) = G * ((i1 + 1),j1) by A8, A23; :: thesis: verum

end;thus [(i1 + 1),j1] in Indices G by A7, A23; :: thesis: ( f /. k = G * (i1,j1) & f /. (k + 1) = G * ((i1 + 1),j1) )

thus f /. k = G * (i1,j1) by A6; :: thesis: f /. (k + 1) = G * ((i1 + 1),j1)

thus f /. (k + 1) = G * ((i1 + 1),j1) by A8, A23; :: thesis: verum

suppose A24:
( i1 = i2 & j2 + 1 = j1 & k <> 1 )
; :: thesis: ( [i1,j1] in Indices G & [(i1 + 1),j1] in Indices G & f /. k = G * (i1,j1) & f /. (k + 1) = G * ((i1 + 1),j1) )

reconsider k9 = k - 1 as Nat by A20, FINSEQ_3:26;

k > 1 by A2, A24, XXREAL_0:1;

then k >= 1 + 1 by NAT_1:13;

then A25: k9 >= (1 + 1) - 1 by XREAL_1:9;

then consider i3, j3, i4, j4 being Nat such that

A26: [i3,j3] in Indices G and

A27: f /. k9 = G * (i3,j3) and

A28: [i4,j4] in Indices G and

A29: f /. (k9 + 1) = G * (i4,j4) and

A30: ( ( 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, A19, JORDAN8:3;

A31: i1 = i4 by A5, A6, A28, A29, GOBOARD1:5;

k9 + 1 < len f by A3, NAT_1:13;

then k9 < len f by NAT_1:13;

then A32: k9 in dom f by A25, FINSEQ_3:25;

A33: 1 <= i3 by A26, MATRIX_0:32;

A34: j3 <= width G by A26, MATRIX_0:32;

A35: j1 = j4 by A5, A6, A28, A29, GOBOARD1:5;

A36: ( i3 <= len G & 1 <= j3 ) by A26, MATRIX_0:32;

A37: i3 = i4

f /. k9 in L~ f by A3, A14, A32, GOBOARD1:1, XXREAL_0:2;

then A42: (G * (i1,j1)) `2 >= (G * (i3,j3)) `2 by A10, A27, PSCOMP_1:24;

end;k > 1 by A2, A24, XXREAL_0:1;

then k >= 1 + 1 by NAT_1:13;

then A25: k9 >= (1 + 1) - 1 by XREAL_1:9;

then consider i3, j3, i4, j4 being Nat such that

A26: [i3,j3] in Indices G and

A27: f /. k9 = G * (i3,j3) and

A28: [i4,j4] in Indices G and

A29: f /. (k9 + 1) = G * (i4,j4) and

A30: ( ( 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, A19, JORDAN8:3;

A31: i1 = i4 by A5, A6, A28, A29, GOBOARD1:5;

k9 + 1 < len f by A3, NAT_1:13;

then k9 < len f by NAT_1:13;

then A32: k9 in dom f by A25, FINSEQ_3:25;

A33: 1 <= i3 by A26, MATRIX_0:32;

A34: j3 <= width G by A26, MATRIX_0:32;

A35: j1 = j4 by A5, A6, A28, A29, GOBOARD1:5;

A36: ( i3 <= len G & 1 <= j3 ) by A26, MATRIX_0:32;

A37: i3 = i4

proof

A41:
k9 + 1 = k
;
assume A38:
i3 <> i4
; :: thesis: contradiction

end;per cases
( ( j3 = j4 & i3 = i4 + 1 ) or ( j3 = j4 & i3 + 1 = i4 ) )
by A30, A38;

end;

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

then
(G * (i3,j3)) `2 <> N-bound (L~ f)
by A1, A19, A25, A26, A27, A28, A29, Th17;

then (G * (1,j3)) `2 <> N-bound (L~ f) by A33, A36, A34, GOBOARD5:1;

then (N-min (L~ f)) `2 <> N-bound (L~ f) by A4, A6, A13, A22, A18, A35, A39, GOBOARD5:1;

hence contradiction by EUCLID:52; :: thesis: verum

end;then (G * (1,j3)) `2 <> N-bound (L~ f) by A33, A36, A34, GOBOARD5:1;

then (N-min (L~ f)) `2 <> N-bound (L~ f) by A4, A6, A13, A22, A18, A35, A39, GOBOARD5:1;

hence contradiction by EUCLID:52; :: thesis: verum

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

(G * (i3,j3)) `2 =
(G * (1,j3)) `2
by A33, A36, A34, GOBOARD5:1

.= (N-min (L~ f)) `2 by A4, A6, A13, A22, A18, A35, A40, GOBOARD5:1

.= N-bound (L~ f) by EUCLID:52 ;

then G * (i3,j3) in N-most (L~ f) by A15, A27, A32, GOBOARD1:1, SPRECT_2:10;

then (G * (i4,j4)) `1 <= (G * (i3,j3)) `1 by A4, A29, PSCOMP_1:39;

then i3 >= i3 + 1 by A22, A18, A31, A35, A33, A40, GOBOARD5:3;

hence contradiction by NAT_1:13; :: thesis: verum

end;.= (N-min (L~ f)) `2 by A4, A6, A13, A22, A18, A35, A40, GOBOARD5:1

.= N-bound (L~ f) by EUCLID:52 ;

then G * (i3,j3) in N-most (L~ f) by A15, A27, A32, GOBOARD1:1, SPRECT_2:10;

then (G * (i4,j4)) `1 <= (G * (i3,j3)) `1 by A4, A29, PSCOMP_1:39;

then i3 >= i3 + 1 by A22, A18, A31, A35, A33, A40, GOBOARD5:3;

hence contradiction by NAT_1:13; :: thesis: verum

f /. k9 in L~ f by A3, A14, A32, GOBOARD1:1, XXREAL_0:2;

then A42: (G * (i1,j1)) `2 >= (G * (i3,j3)) `2 by A10, A27, PSCOMP_1:24;

now :: thesis: contradictionend;

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: verumper cases
( j4 + 1 = j3 or j4 = j3 + 1 )
by A30, A37;

end;

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

then
j4 >= j4 + 1
by A13, A22, A31, A35, A34, A42, A37, GOBOARD5:4;

hence contradiction by NAT_1:13; :: thesis: verum

end;hence contradiction by NAT_1:13; :: thesis: verum

suppose A43:
j4 = j3 + 1
; :: thesis: contradiction

k9 + (1 + 1) <= len f
by A3;

then A44: (LSeg (f,k9)) /\ (LSeg (f,k)) = {(f /. k)} by A25, A41, TOPREAL1:def 6;

( f /. k9 in LSeg (f,k9) & f /. (k + 1) in LSeg (f,k) ) by A2, A3, A19, A25, A41, TOPREAL1:21;

then f /. (k + 1) in {(f /. k)} by A8, A24, A27, A31, A35, A37, A43, A44, XBOOLE_0:def 4;

then A45: f /. (k + 1) = f /. k by TARSKI:def 1;

j1 <> j2 by A24;

hence contradiction by A5, A6, A7, A8, A45, GOBOARD1:5; :: thesis: verum

end;then A44: (LSeg (f,k9)) /\ (LSeg (f,k)) = {(f /. k)} by A25, A41, TOPREAL1:def 6;

( f /. k9 in LSeg (f,k9) & f /. (k + 1) in LSeg (f,k) ) by A2, A3, A19, A25, A41, TOPREAL1:21;

then f /. (k + 1) in {(f /. k)} by A8, A24, A27, A31, A35, A37, A43, A44, XBOOLE_0:def 4;

then A45: f /. (k + 1) = f /. k by TARSKI:def 1;

j1 <> j2 by A24;

hence contradiction by A5, A6, A7, A8, A45, GOBOARD1:5; :: thesis: verum

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

set k1 = len f;

k < len f by A3, NAT_1:13;

then A47: len f > 1 + 0 by A2, XXREAL_0:2;

then len f in dom f by FINSEQ_3:25;

then reconsider k9 = (len f) - 1 as Nat by FINSEQ_3:26;

k + 1 >= 1 + 1 by A2, XREAL_1:7;

then len f >= 1 + 1 by A3, XXREAL_0:2;

then A48: k9 >= (1 + 1) - 1 by XREAL_1:9;

then consider i3, j3, i4, j4 being Nat such that

A49: [i3,j3] in Indices G and

A50: f /. k9 = G * (i3,j3) and

A51: [i4,j4] in Indices G and

A52: f /. (k9 + 1) = G * (i4,j4) and

A53: ( ( 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, JORDAN8:3;

A54: f /. (len f) = f /. 1 by FINSEQ_6:def 1;

then A55: i1 = i4 by A5, A6, A46, A51, A52, GOBOARD1:5;

k9 + 1 <= len f ;

then k9 < len f by NAT_1:13;

then A56: k9 in dom f by A48, FINSEQ_3:25;

then f /. k9 in L~ f by A3, A14, GOBOARD1:1, XXREAL_0:2;

then A57: (G * (i1,j1)) `2 >= (G * (i3,j3)) `2 by A10, A50, PSCOMP_1:24;

A58: 1 <= i3 by A49, MATRIX_0:32;

A59: j1 = j4 by A5, A6, A46, A54, A51, A52, GOBOARD1:5;

A60: j3 <= width G by A49, MATRIX_0:32;

A61: ( i3 <= len G & 1 <= j3 ) by A49, MATRIX_0:32;

A62: i3 = i4

end;k < len f by A3, NAT_1:13;

then A47: len f > 1 + 0 by A2, XXREAL_0:2;

then len f in dom f by FINSEQ_3:25;

then reconsider k9 = (len f) - 1 as Nat by FINSEQ_3:26;

k + 1 >= 1 + 1 by A2, XREAL_1:7;

then len f >= 1 + 1 by A3, XXREAL_0:2;

then A48: k9 >= (1 + 1) - 1 by XREAL_1:9;

then consider i3, j3, i4, j4 being Nat such that

A49: [i3,j3] in Indices G and

A50: f /. k9 = G * (i3,j3) and

A51: [i4,j4] in Indices G and

A52: f /. (k9 + 1) = G * (i4,j4) and

A53: ( ( 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, JORDAN8:3;

A54: f /. (len f) = f /. 1 by FINSEQ_6:def 1;

then A55: i1 = i4 by A5, A6, A46, A51, A52, GOBOARD1:5;

k9 + 1 <= len f ;

then k9 < len f by NAT_1:13;

then A56: k9 in dom f by A48, FINSEQ_3:25;

then f /. k9 in L~ f by A3, A14, GOBOARD1:1, XXREAL_0:2;

then A57: (G * (i1,j1)) `2 >= (G * (i3,j3)) `2 by A10, A50, PSCOMP_1:24;

A58: 1 <= i3 by A49, MATRIX_0:32;

A59: j1 = j4 by A5, A6, A46, A54, A51, A52, GOBOARD1:5;

A60: j3 <= width G by A49, MATRIX_0:32;

A61: ( i3 <= len G & 1 <= j3 ) by A49, MATRIX_0:32;

A62: i3 = i4

proof

A66:
k9 + 1 = len f
;
assume A63:
i3 <> i4
; :: thesis: contradiction

end;per cases
( ( j3 = j4 & i3 = i4 + 1 ) or ( j3 = j4 & i3 + 1 = i4 ) )
by A53, A63;

end;

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

then
(G * (i3,j3)) `2 <> N-bound (L~ f)
by A1, A48, A49, A50, A51, A52, Th17;

then (G * (1,j3)) `2 <> N-bound (L~ f) by A58, A61, A60, GOBOARD5:1;

then (N-min (L~ f)) `2 <> N-bound (L~ f) by A4, A6, A13, A22, A18, A59, A64, GOBOARD5:1;

hence contradiction by EUCLID:52; :: thesis: verum

end;then (G * (1,j3)) `2 <> N-bound (L~ f) by A58, A61, A60, GOBOARD5:1;

then (N-min (L~ f)) `2 <> N-bound (L~ f) by A4, A6, A13, A22, A18, A59, A64, GOBOARD5:1;

hence contradiction by EUCLID:52; :: thesis: verum

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

(G * (i3,j3)) `2 =
(G * (1,j3)) `2
by A58, A61, A60, GOBOARD5:1

.= (N-min (L~ f)) `2 by A4, A6, A13, A22, A18, A59, A65, GOBOARD5:1

.= N-bound (L~ f) by EUCLID:52 ;

then G * (i3,j3) in N-most (L~ f) by A15, A50, A56, GOBOARD1:1, SPRECT_2:10;

then (G * (i4,j4)) `1 <= (G * (i3,j3)) `1 by A4, A46, A54, A52, PSCOMP_1:39;

then i3 >= i3 + 1 by A22, A18, A55, A59, A58, A65, GOBOARD5:3;

hence contradiction by NAT_1:13; :: thesis: verum

end;.= (N-min (L~ f)) `2 by A4, A6, A13, A22, A18, A59, A65, GOBOARD5:1

.= N-bound (L~ f) by EUCLID:52 ;

then G * (i3,j3) in N-most (L~ f) by A15, A50, A56, GOBOARD1:1, SPRECT_2:10;

then (G * (i4,j4)) `1 <= (G * (i3,j3)) `1 by A4, A46, A54, A52, PSCOMP_1:39;

then i3 >= i3 + 1 by A22, A18, A55, A59, A58, A65, GOBOARD5:3;

hence contradiction by NAT_1:13; :: thesis: verum

now :: thesis: contradictionend;

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: verumper cases
( j4 + 1 = j3 or j4 = j3 + 1 )
by A53, A62;

end;

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

then
j4 >= j4 + 1
by A13, A22, A55, A59, A60, A57, A62, GOBOARD5:4;

hence contradiction by NAT_1:13; :: thesis: verum

end;hence contradiction by NAT_1:13; :: thesis: verum

suppose A67:
j4 = j3 + 1
; :: thesis: contradiction

(len f) - 1 >= 0
by A47, XREAL_1:19;

then (len f) -' 1 = (len f) - 1 by XREAL_0:def 2;

then A68: (LSeg (f,k)) /\ (LSeg (f,k9)) = {(f . k)} by A46, JORDAN4:42

.= {(f /. k)} by A20, PARTFUN1:def 6 ;

( f /. k9 in LSeg (f,k9) & f /. (k + 1) in LSeg (f,k) ) by A2, A3, A48, A66, TOPREAL1:21;

then f /. (k + 1) in {(f /. k)} by A8, A46, A50, A55, A59, A62, A67, A68, XBOOLE_0:def 4;

then A69: f /. (k + 1) = f /. k by TARSKI:def 1;

j1 <> j2 by A46;

hence contradiction by A5, A6, A7, A8, A69, GOBOARD1:5; :: thesis: verum

end;then (len f) -' 1 = (len f) - 1 by XREAL_0:def 2;

then A68: (LSeg (f,k)) /\ (LSeg (f,k9)) = {(f . k)} by A46, JORDAN4:42

.= {(f /. k)} by A20, PARTFUN1:def 6 ;

( f /. k9 in LSeg (f,k9) & f /. (k + 1) in LSeg (f,k) ) by A2, A3, A48, A66, TOPREAL1:21;

then f /. (k + 1) in {(f /. k)} by A8, A46, A50, A55, A59, A62, A67, A68, XBOOLE_0:def 4;

then A69: f /. (k + 1) = f /. k by TARSKI:def 1;

j1 <> j2 by A46;

hence contradiction by A5, A6, A7, A8, A69, GOBOARD1:5; :: thesis: verum

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

then
j1 >= j1 + 1
by A13, A22, A11, A17, 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: verum

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) ) by NAT_1:13; :: thesis: verum

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

(G * (i2,j2)) `2 =
(G * (1,j2)) `2
by A12, A21, A11, GOBOARD5:1

.= N-bound (L~ f) by A13, A22, A18, A10, A70, GOBOARD5:1 ;

then G * (i2,j2) in N-most (L~ f) by A8, A15, A16, GOBOARD1:1, SPRECT_2:10;

then (G * (i1,j1)) `1 <= (G * (i2,j2)) `1 by A4, A6, PSCOMP_1:39;

then i2 >= i2 + 1 by A22, A18, A12, A70, GOBOARD5:3;

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: verum

end;.= N-bound (L~ f) by A13, A22, A18, A10, A70, GOBOARD5:1 ;

then G * (i2,j2) in N-most (L~ f) by A8, A15, A16, GOBOARD1:1, SPRECT_2:10;

then (G * (i1,j1)) `1 <= (G * (i2,j2)) `1 by A4, A6, PSCOMP_1:39;

then i2 >= i2 + 1 by A22, A18, A12, A70, GOBOARD5:3;

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: verum