let f be FinSequence of (TOP-REAL 2); :: thesis: for G being Go-board st f is special holds

for n being Nat st n in dom f & n + 1 in dom f holds

for i, j, m, k being Nat st [i,j] in Indices G & [m,k] in Indices G & f /. n = G * (i,j) & f /. (n + 1) = G * (m,k) & not i = m holds

k = j

let G be Go-board; :: thesis: ( f is special implies for n being Nat st n in dom f & n + 1 in dom f holds

for i, j, m, k being Nat st [i,j] in Indices G & [m,k] in Indices G & f /. n = G * (i,j) & f /. (n + 1) = G * (m,k) & not i = m holds

k = j )

assume A1: f is special ; :: thesis: for n being Nat st n in dom f & n + 1 in dom f holds

for i, j, m, k being Nat st [i,j] in Indices G & [m,k] in Indices G & f /. n = G * (i,j) & f /. (n + 1) = G * (m,k) & not i = m holds

k = j

let n be Nat; :: thesis: ( n in dom f & n + 1 in dom f implies for i, j, m, k being Nat st [i,j] in Indices G & [m,k] in Indices G & f /. n = G * (i,j) & f /. (n + 1) = G * (m,k) & not i = m holds

k = j )

assume ( n in dom f & n + 1 in dom f ) ; :: thesis: for i, j, m, k being Nat st [i,j] in Indices G & [m,k] in Indices G & f /. n = G * (i,j) & f /. (n + 1) = G * (m,k) & not i = m holds

k = j

then A2: ( 1 <= n & n + 1 <= len f ) by FINSEQ_3:25;

let i, j, m, k be Nat; :: thesis: ( [i,j] in Indices G & [m,k] in Indices G & f /. n = G * (i,j) & f /. (n + 1) = G * (m,k) & not i = m implies k = j )

assume that

A3: [i,j] in Indices G and

A4: [m,k] in Indices G and

A5: ( f /. n = G * (i,j) & f /. (n + 1) = G * (m,k) ) ; :: thesis: ( i = m or k = j )

reconsider cj = Col (G,j), lm = Line (G,m) as FinSequence of (TOP-REAL 2) ;

set xj = X_axis cj;

set yj = Y_axis cj;

set xm = X_axis lm;

set ym = Y_axis lm;

len cj = len G by MATRIX_0:def 8;

then A6: dom cj = dom G by FINSEQ_3:29;

assume that

A7: i <> m and

A8: k <> j ; :: thesis: contradiction

A9: ( len (X_axis lm) = len lm & dom (X_axis lm) = Seg (len (X_axis lm)) ) by FINSEQ_1:def 3, GOBOARD1:def 1;

A10: len (X_axis cj) = len cj by GOBOARD1:def 1;

then A11: dom (X_axis cj) = dom cj by FINSEQ_3:29;

A12: Indices G = [:(dom G),(Seg (width G)):] by MATRIX_0:def 4;

then A13: i in dom G by A3, ZFMISC_1:87;

then cj /. i = cj . i by A6, PARTFUN1:def 6;

then A14: G * (i,j) = cj /. i by A13, MATRIX_0:def 8;

then A15: (X_axis cj) . i = (G * (i,j)) `1 by A13, A6, A11, GOBOARD1:def 1;

A16: m in dom G by A4, A12, ZFMISC_1:87;

then cj /. m = cj . m by A6, PARTFUN1:def 6;

then A17: G * (m,j) = cj /. m by A16, MATRIX_0:def 8;

then A18: (X_axis cj) . m = (G * (m,j)) `1 by A16, A6, A11, GOBOARD1:def 1;

A19: Y_axis lm is increasing by A16, GOBOARD1:def 6;

A20: X_axis lm is constant by A16, GOBOARD1:def 4;

A21: dom (Y_axis cj) = Seg (len (Y_axis cj)) by FINSEQ_1:def 3;

A22: ( dom (X_axis cj) = Seg (len (X_axis cj)) & len (Y_axis cj) = len cj ) by FINSEQ_1:def 3, GOBOARD1:def 2;

then A23: (Y_axis cj) . m = (G * (m,j)) `2 by A16, A10, A21, A6, A11, A17, GOBOARD1:def 2;

A24: j in Seg (width G) by A3, A12, ZFMISC_1:87;

then A25: X_axis cj is increasing by GOBOARD1:def 7;

A26: len lm = width G by MATRIX_0:def 7;

then A27: dom lm = Seg (width G) by FINSEQ_1:def 3;

then lm /. j = lm . j by A24, PARTFUN1:def 6;

then A28: G * (m,j) = lm /. j by A24, MATRIX_0:def 7;

then A29: (X_axis lm) . j = (G * (m,j)) `1 by A24, A26, A9, GOBOARD1:def 1;

A30: k in Seg (width G) by A4, A12, ZFMISC_1:87;

then lm /. k = lm . k by A27, PARTFUN1:def 6;

then A31: G * (m,k) = lm /. k by A30, MATRIX_0:def 7;

then A32: (X_axis lm) . k = (G * (m,k)) `1 by A30, A26, A9, GOBOARD1:def 1;

A33: Y_axis cj is constant by A24, GOBOARD1:def 5;

A34: ( len (Y_axis lm) = len lm & dom (Y_axis lm) = Seg (len (Y_axis lm)) ) by FINSEQ_1:def 3, GOBOARD1:def 2;

then A35: (Y_axis lm) . j = (G * (m,j)) `2 by A24, A26, A28, GOBOARD1:def 2;

A36: (Y_axis lm) . k = (G * (m,k)) `2 by A30, A26, A34, A31, GOBOARD1:def 2;

A37: (Y_axis cj) . i = (G * (i,j)) `2 by A13, A10, A22, A21, A6, A11, A14, GOBOARD1:def 2;

for n being Nat st n in dom f & n + 1 in dom f holds

for i, j, m, k being Nat st [i,j] in Indices G & [m,k] in Indices G & f /. n = G * (i,j) & f /. (n + 1) = G * (m,k) & not i = m holds

k = j

let G be Go-board; :: thesis: ( f is special implies for n being Nat st n in dom f & n + 1 in dom f holds

for i, j, m, k being Nat st [i,j] in Indices G & [m,k] in Indices G & f /. n = G * (i,j) & f /. (n + 1) = G * (m,k) & not i = m holds

k = j )

assume A1: f is special ; :: thesis: for n being Nat st n in dom f & n + 1 in dom f holds

for i, j, m, k being Nat st [i,j] in Indices G & [m,k] in Indices G & f /. n = G * (i,j) & f /. (n + 1) = G * (m,k) & not i = m holds

k = j

let n be Nat; :: thesis: ( n in dom f & n + 1 in dom f implies for i, j, m, k being Nat st [i,j] in Indices G & [m,k] in Indices G & f /. n = G * (i,j) & f /. (n + 1) = G * (m,k) & not i = m holds

k = j )

assume ( n in dom f & n + 1 in dom f ) ; :: thesis: for i, j, m, k being Nat st [i,j] in Indices G & [m,k] in Indices G & f /. n = G * (i,j) & f /. (n + 1) = G * (m,k) & not i = m holds

k = j

then A2: ( 1 <= n & n + 1 <= len f ) by FINSEQ_3:25;

let i, j, m, k be Nat; :: thesis: ( [i,j] in Indices G & [m,k] in Indices G & f /. n = G * (i,j) & f /. (n + 1) = G * (m,k) & not i = m implies k = j )

assume that

A3: [i,j] in Indices G and

A4: [m,k] in Indices G and

A5: ( f /. n = G * (i,j) & f /. (n + 1) = G * (m,k) ) ; :: thesis: ( i = m or k = j )

reconsider cj = Col (G,j), lm = Line (G,m) as FinSequence of (TOP-REAL 2) ;

set xj = X_axis cj;

set yj = Y_axis cj;

set xm = X_axis lm;

set ym = Y_axis lm;

len cj = len G by MATRIX_0:def 8;

then A6: dom cj = dom G by FINSEQ_3:29;

assume that

A7: i <> m and

A8: k <> j ; :: thesis: contradiction

A9: ( len (X_axis lm) = len lm & dom (X_axis lm) = Seg (len (X_axis lm)) ) by FINSEQ_1:def 3, GOBOARD1:def 1;

A10: len (X_axis cj) = len cj by GOBOARD1:def 1;

then A11: dom (X_axis cj) = dom cj by FINSEQ_3:29;

A12: Indices G = [:(dom G),(Seg (width G)):] by MATRIX_0:def 4;

then A13: i in dom G by A3, ZFMISC_1:87;

then cj /. i = cj . i by A6, PARTFUN1:def 6;

then A14: G * (i,j) = cj /. i by A13, MATRIX_0:def 8;

then A15: (X_axis cj) . i = (G * (i,j)) `1 by A13, A6, A11, GOBOARD1:def 1;

A16: m in dom G by A4, A12, ZFMISC_1:87;

then cj /. m = cj . m by A6, PARTFUN1:def 6;

then A17: G * (m,j) = cj /. m by A16, MATRIX_0:def 8;

then A18: (X_axis cj) . m = (G * (m,j)) `1 by A16, A6, A11, GOBOARD1:def 1;

A19: Y_axis lm is increasing by A16, GOBOARD1:def 6;

A20: X_axis lm is constant by A16, GOBOARD1:def 4;

A21: dom (Y_axis cj) = Seg (len (Y_axis cj)) by FINSEQ_1:def 3;

A22: ( dom (X_axis cj) = Seg (len (X_axis cj)) & len (Y_axis cj) = len cj ) by FINSEQ_1:def 3, GOBOARD1:def 2;

then A23: (Y_axis cj) . m = (G * (m,j)) `2 by A16, A10, A21, A6, A11, A17, GOBOARD1:def 2;

A24: j in Seg (width G) by A3, A12, ZFMISC_1:87;

then A25: X_axis cj is increasing by GOBOARD1:def 7;

A26: len lm = width G by MATRIX_0:def 7;

then A27: dom lm = Seg (width G) by FINSEQ_1:def 3;

then lm /. j = lm . j by A24, PARTFUN1:def 6;

then A28: G * (m,j) = lm /. j by A24, MATRIX_0:def 7;

then A29: (X_axis lm) . j = (G * (m,j)) `1 by A24, A26, A9, GOBOARD1:def 1;

A30: k in Seg (width G) by A4, A12, ZFMISC_1:87;

then lm /. k = lm . k by A27, PARTFUN1:def 6;

then A31: G * (m,k) = lm /. k by A30, MATRIX_0:def 7;

then A32: (X_axis lm) . k = (G * (m,k)) `1 by A30, A26, A9, GOBOARD1:def 1;

A33: Y_axis cj is constant by A24, GOBOARD1:def 5;

A34: ( len (Y_axis lm) = len lm & dom (Y_axis lm) = Seg (len (Y_axis lm)) ) by FINSEQ_1:def 3, GOBOARD1:def 2;

then A35: (Y_axis lm) . j = (G * (m,j)) `2 by A24, A26, A28, GOBOARD1:def 2;

A36: (Y_axis lm) . k = (G * (m,k)) `2 by A30, A26, A34, A31, GOBOARD1:def 2;

A37: (Y_axis cj) . i = (G * (i,j)) `2 by A13, A10, A22, A21, A6, A11, A14, GOBOARD1:def 2;

now :: thesis: contradictionend;

hence
contradiction
; :: thesis: verumper cases
( (G * (i,j)) `1 = (G * (m,k)) `1 or (G * (i,j)) `2 = (G * (m,k)) `2 )
by A1, A5, A2;

end;

suppose A38:
(G * (i,j)) `1 = (G * (m,k)) `1
; :: thesis: contradiction

end;

now :: thesis: contradiction

hence
contradiction
; :: thesis: verumend;

suppose A39:
(G * (i,j)) `2 = (G * (m,k)) `2
; :: thesis: contradiction

end;

now :: thesis: contradiction

hence
contradiction
; :: thesis: verumend;