let f be FinSequence of (TOP-REAL 2); :: thesis: for G being Go-board st f is special holds
for n being Element of NAT st n in dom f & n + 1 in dom f holds
for i, j, m, k being Element of 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 Element of NAT st n in dom f & n + 1 in dom f holds
for i, j, m, k being Element of 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 Element of NAT st n in dom f & n + 1 in dom f holds
for i, j, m, k being Element of 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 Element of NAT ; :: thesis: ( n in dom f & n + 1 in dom f implies for i, j, m, k being Element of 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 A2: ( n in dom f & n + 1 in dom f ) ; :: thesis: for i, j, m, k being Element of 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 i, j, m, k be Element of 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 A3: ( [i,j] in Indices G & [m,k] in Indices G & f /. n = G * i,j & f /. (n + 1) = G * m,k ) ; :: thesis: ( i = m or k = j )
assume A4: ( i <> m & k <> j ) ; :: thesis: contradiction
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;
Indices G = [:(dom G),(Seg (width G)):] by MATRIX_1:def 5;
then A5: ( i in dom G & j in Seg (width G) & m in dom G & k in Seg (width G) & len cj = len G & len (X_axis cj) = len cj & dom (X_axis cj) = Seg (len (X_axis cj)) & len lm = width G & len (X_axis lm) = len lm & dom (X_axis lm) = Seg (len (X_axis lm)) & len (Y_axis cj) = len cj & dom (Y_axis cj) = Seg (len (Y_axis cj)) & len (Y_axis lm) = len lm & dom (Y_axis lm) = Seg (len (Y_axis lm)) ) by A3, FINSEQ_1:def 3, GOBOARD1:def 3, GOBOARD1:def 4, MATRIX_1:def 8, MATRIX_1:def 9, ZFMISC_1:106;
then A6: ( dom cj = dom G & dom lm = Seg (width G) & dom (X_axis cj) = dom cj & dom (X_axis lm) = dom lm & dom (Y_axis cj) = dom cj & dom (Y_axis lm) = dom lm ) by FINSEQ_3:31;
then ( cj /. i = cj . i & cj /. m = cj . m & lm /. j = lm . j & lm /. k = lm . k ) by A5, PARTFUN1:def 8;
then ( G * i,j = cj /. i & G * m,j = cj /. m & G * m,j = lm /. j & G * m,k = lm /. k ) by A5, MATRIX_1:def 8, MATRIX_1:def 9;
then A7: ( X_axis cj is increasing & (X_axis cj) . i = (G * i,j) `1 & (X_axis cj) . m = (G * m,j) `1 & X_axis lm is constant & (X_axis lm) . j = (G * m,j) `1 & (X_axis lm) . k = (G * m,k) `1 & Y_axis lm is increasing & (Y_axis lm) . j = (G * m,j) `2 & (Y_axis lm) . k = (G * m,k) `2 & Y_axis cj is constant & (Y_axis cj) . i = (G * i,j) `2 & (Y_axis cj) . m = (G * m,j) `2 ) by A5, A6, GOBOARD1:def 3, GOBOARD1:def 4, GOBOARD1:def 6, GOBOARD1:def 7, GOBOARD1:def 8, GOBOARD1:def 9;
A8: ( 1 <= n & n + 1 <= len f ) by A2, FINSEQ_3:27;

now

per cases ( (G * i,j) `1 = (G * m,k) `1 or (G * i,j) `2 = (G * m,k) `2 ) by A1, A3, A8, TOPREAL1:def 7;

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

now

per cases ( i > m or i < m ) by A4, XXREAL_0:1;

suppose i > m ; :: thesis: contradiction

then (G * m,j) `1 < (G * i,j) `1 by A5, A6, A7, SEQM_3:def 1;
hence contradiction by A5, A7, A9, GOBOARD1:def 2; :: thesis: verum

end;

suppose i < m ; :: thesis: contradiction

then (G * m,j) `1 > (G * i,j) `1 by A5, A6, A7, SEQM_3:def 1;
hence contradiction by A5, A7, A9, GOBOARD1:def 2; :: thesis: verum

end;

end;

end;

hence contradiction ; :: thesis: verum

end;

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

now

per cases ( k > j or k < j ) by A4, XXREAL_0:1;

suppose k > j ; :: thesis: contradiction

then (G * m,j) `2 < (G * m,k) `2 by A5, A7, SEQM_3:def 1;
hence contradiction by A5, A6, A7, A10, GOBOARD1:def 2; :: thesis: verum

end;

suppose k < j ; :: thesis: contradiction

then (G * m,j) `2 > (G * m,k) `2 by A5, A7, SEQM_3:def 1;
hence contradiction by A5, A6, A7, A10, GOBOARD1:def 2; :: thesis: verum

end;

end;

end;

hence contradiction ; :: thesis: verum

end;

end;

end;

hence contradiction ; :: thesis: verum