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;
hence contradiction ; :: thesis: verum