let f be FinSequence of (); :: 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 () ;
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 ;
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 ()):] by MATRIX_0:def 4;
then A13: i in dom G by ;
then cj /. i = cj . i by ;
then A14: G * (i,j) = cj /. i by ;
then A15: (X_axis cj) . i = (G * (i,j)) `1 by ;
A16: m in dom G by ;
then cj /. m = cj . m by ;
then A17: G * (m,j) = cj /. m by ;
then A18: (X_axis cj) . m = (G * (m,j)) `1 by ;
A19: Y_axis lm is increasing by ;
A20: X_axis lm is constant by ;
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 ;
then A23: (Y_axis cj) . m = (G * (m,j)) `2 by ;
A24: j in Seg () by ;
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 () by FINSEQ_1:def 3;
then lm /. j = lm . j by ;
then A28: G * (m,j) = lm /. j by ;
then A29: (X_axis lm) . j = (G * (m,j)) `1 by ;
A30: k in Seg () by ;
then lm /. k = lm . k by ;
then A31: G * (m,k) = lm /. k by ;
then A32: (X_axis lm) . k = (G * (m,k)) `1 by ;
A33: Y_axis cj is constant by ;
A34: ( len (Y_axis lm) = len lm & dom (Y_axis lm) = Seg (len (Y_axis lm)) ) by ;
then A35: (Y_axis lm) . j = (G * (m,j)) `2 by ;
A36: (Y_axis lm) . k = (G * (m,k)) `2 by ;
A37: (Y_axis cj) . i = (G * (i,j)) `2 by ;
now :: thesis: contradiction
per cases ( (G * (i,j)) `1 = (G * (m,k)) `1 or (G * (i,j)) `2 = (G * (m,k)) `2 ) by A1, A5, A2;
suppose A38: (G * (i,j)) `1 = (G * (m,k)) `1 ; :: thesis: contradiction
now :: thesis: contradiction
per cases ( i > m or i < m ) by ;
suppose i > m ; :: thesis: contradiction
then (G * (m,j)) `1 < (G * (i,j)) `1 by ;
hence contradiction by A24, A30, A26, A9, A20, A29, A32, A38, SEQM_3:def 10; :: thesis: verum
end;
suppose i < m ; :: thesis: contradiction
then (G * (m,j)) `1 > (G * (i,j)) `1 by ;
hence contradiction by A24, A30, A26, A9, A20, A29, A32, A38, SEQM_3:def 10; :: thesis: verum
end;
end;
end;
hence contradiction ; :: thesis: verum
end;
suppose A39: (G * (i,j)) `2 = (G * (m,k)) `2 ; :: thesis: contradiction
now :: thesis: contradiction
per cases ( k > j or k < j ) by ;
suppose k > j ; :: thesis: contradiction
then (G * (m,j)) `2 < (G * (m,k)) `2 by ;
hence contradiction by A13, A16, A10, A22, A21, A6, A11, A33, A37, A23, A39, SEQM_3:def 10; :: thesis: verum
end;
suppose k < j ; :: thesis: contradiction
then (G * (m,j)) `2 > (G * (m,k)) `2 by ;
hence contradiction by A13, A16, A10, A22, A21, A6, A11, A33, A37, A23, A39, SEQM_3:def 10; :: thesis: verum
end;
end;
end;
hence contradiction ; :: thesis: verum
end;
end;
end;
hence contradiction ; :: thesis: verum