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 ( 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
then A2: ( 1 <= n & n + 1 <= len f ) by FINSEQ_3:27;
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 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_1:def 9;
then A6: dom cj = dom G by FINSEQ_3:31;
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 3;
A10: len (X_axis cj) = len cj by GOBOARD1:def 3;
then A11: dom (X_axis cj) = dom cj by FINSEQ_3:31;
A12: Indices G = [:(dom G),(Seg (width G)):] by MATRIX_1:def 5;
then A13: i in dom G by A3, ZFMISC_1:106;
then cj /. i = cj . i by A6, PARTFUN1:def 8;
then A14: G * i,j = cj /. i by A13, MATRIX_1:def 9;
then A15: (X_axis cj) . i = (G * i,j) `1 by A13, A6, A11, GOBOARD1:def 3;
A16: m in dom G by A4, A12, ZFMISC_1:106;
then cj /. m = cj . m by A6, PARTFUN1:def 8;
then A17: G * m,j = cj /. m by A16, MATRIX_1:def 9;
then A18: (X_axis cj) . m = (G * m,j) `1 by A16, A6, A11, GOBOARD1:def 3;
A19: Y_axis lm is increasing by A16, GOBOARD1:def 8;
A20: X_axis lm is constant by A16, GOBOARD1:def 6;
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 4;
then A23: (Y_axis cj) . m = (G * m,j) `2 by A16, A10, A21, A6, A11, A17, GOBOARD1:def 4;
A24: j in Seg (width G) by A3, A12, ZFMISC_1:106;
then A25: X_axis cj is increasing by GOBOARD1:def 9;
A26: len lm = width G by MATRIX_1:def 8;
then A27: dom lm = Seg (width G) by FINSEQ_1:def 3;
then lm /. j = lm . j by A24, PARTFUN1:def 8;
then A28: G * m,j = lm /. j by A24, MATRIX_1:def 8;
then A29: (X_axis lm) . j = (G * m,j) `1 by A24, A26, A9, GOBOARD1:def 3;
A30: k in Seg (width G) by A4, A12, ZFMISC_1:106;
then lm /. k = lm . k by A27, PARTFUN1:def 8;
then A31: G * m,k = lm /. k by A30, MATRIX_1:def 8;
then A32: (X_axis lm) . k = (G * m,k) `1 by A30, A26, A9, GOBOARD1:def 3;
A33: Y_axis cj is constant by A24, GOBOARD1:def 7;
A34: ( len (Y_axis lm) = len lm & dom (Y_axis lm) = Seg (len (Y_axis lm)) ) by FINSEQ_1:def 3, GOBOARD1:def 4;
then A35: (Y_axis lm) . j = (G * m,j) `2 by A24, A26, A28, GOBOARD1:def 4;
A36: (Y_axis lm) . k = (G * m,k) `2 by A30, A26, A34, A31, GOBOARD1:def 4;
A37: (Y_axis cj) . i = (G * i,j) `2 by A13, A10, A22, A21, A6, A11, A14, GOBOARD1:def 4;

now

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

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

now

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

suppose i > m ; :: thesis: contradiction

then (G * m,j) `1 < (G * i,j) `1 by A13, A16, A6, A11, A25, A15, A18, SEQM_3:def 1;
hence contradiction by A24, A30, A26, A9, A20, A29, A32, A38, SEQM_3:def 15; :: thesis: verum

end;

suppose i < m ; :: thesis: contradiction

then (G * m,j) `1 > (G * i,j) `1 by A13, A16, A6, A11, A25, A15, A18, SEQM_3:def 1;
hence contradiction by A24, A30, A26, A9, A20, A29, A32, A38, SEQM_3:def 15; :: thesis: verum

end;

end;

end;

hence contradiction ; :: thesis: verum

end;

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

now

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

suppose k > j ; :: thesis: contradiction

then (G * m,j) `2 < (G * m,k) `2 by A24, A30, A26, A34, A19, A35, A36, SEQM_3:def 1;
hence contradiction by A13, A16, A10, A22, A21, A6, A11, A33, A37, A23, A39, SEQM_3:def 15; :: thesis: verum

end;

suppose k < j ; :: thesis: contradiction

then (G * m,j) `2 > (G * m,k) `2 by A24, A30, A26, A34, A19, A35, A36, SEQM_3:def 1;
hence contradiction by A13, A16, A10, A22, A21, A6, A11, A33, A37, A23, A39, SEQM_3:def 15; :: thesis: verum

end;

end;

end;

hence contradiction ; :: thesis: verum

end;

end;

end;

hence contradiction ; :: thesis: verum