let i be Nat; :: thesis: for G being Go-board
for f being FinSequence of () st f is_sequence_on G & i in Seg () & rng f misses rng (Col (G,i)) & width G > 1 holds
f is_sequence_on DelCol (G,i)

let G be Go-board; :: thesis: for f being FinSequence of () st f is_sequence_on G & i in Seg () & rng f misses rng (Col (G,i)) & width G > 1 holds
f is_sequence_on DelCol (G,i)

let f be FinSequence of (); :: thesis: ( f is_sequence_on G & i in Seg () & rng f misses rng (Col (G,i)) & width G > 1 implies f is_sequence_on DelCol (G,i) )
set D = DelCol (G,i);
assume that
A1: f is_sequence_on G and
A2: i in Seg () and
A3: rng f misses rng (Col (G,i)) and
A4: width G > 1 ; :: thesis: f is_sequence_on DelCol (G,i)
A5: len G = len (DelCol (G,i)) by MATRIX_0:def 13;
A6: Indices (DelCol (G,i)) = [:(dom (DelCol (G,i))),(Seg (width (DelCol (G,i)))):] by MATRIX_0:def 4;
A7: Indices G = [:(dom G),(Seg ()):] by MATRIX_0:def 4;
A8: ( dom G = Seg (len G) & dom (DelCol (G,i)) = Seg (len (DelCol (G,i))) ) by FINSEQ_1:def 3;
consider M being Nat such that
A9: width G = M + 1 and
A10: M > 0 by ;
A11: width (DelCol (G,i)) = M by ;
A12: now :: thesis: for n being Nat st n in dom f & n + 1 in dom f holds
for i1, i2, j1, j2 being Nat st [i1,i2] in Indices (DelCol (G,i)) & [j1,j2] in Indices (DelCol (G,i)) & f /. n = (DelCol (G,i)) * (i1,i2) & f /. (n + 1) = (DelCol (G,i)) * (j1,j2) holds
|.(i1 - j1).| + |.(i2 - j2).| = 1
let n be Nat; :: thesis: ( n in dom f & n + 1 in dom f implies for i1, i2, j1, j2 being Nat st [i1,i2] in Indices (DelCol (G,i)) & [j1,j2] in Indices (DelCol (G,i)) & f /. n = (DelCol (G,i)) * (i1,i2) & f /. (n + 1) = (DelCol (G,i)) * (j1,j2) holds
|.(i1 - j1).| + |.(i2 - j2).| = 1 )

assume A13: ( n in dom f & n + 1 in dom f ) ; :: thesis: for i1, i2, j1, j2 being Nat st [i1,i2] in Indices (DelCol (G,i)) & [j1,j2] in Indices (DelCol (G,i)) & f /. n = (DelCol (G,i)) * (i1,i2) & f /. (n + 1) = (DelCol (G,i)) * (j1,j2) holds
|.(i1 - j1).| + |.(i2 - j2).| = 1

let i1, i2, j1, j2 be Nat; :: thesis: ( [i1,i2] in Indices (DelCol (G,i)) & [j1,j2] in Indices (DelCol (G,i)) & f /. n = (DelCol (G,i)) * (i1,i2) & f /. (n + 1) = (DelCol (G,i)) * (j1,j2) implies |.(i1 - j1).| + |.(i2 - j2).| = 1 )
assume that
A14: [i1,i2] in Indices (DelCol (G,i)) and
A15: [j1,j2] in Indices (DelCol (G,i)) and
A16: ( f /. n = (DelCol (G,i)) * (i1,i2) & f /. (n + 1) = (DelCol (G,i)) * (j1,j2) ) ; :: thesis: |.(i1 - j1).| + |.(i2 - j2).| = 1
A17: i1 in dom (DelCol (G,i)) by ;
A18: i2 in Seg (width (DelCol (G,i))) by ;
then A19: 1 <= i2 by FINSEQ_1:1;
A20: i2 <= M by ;
then ( 1 <= i2 + 1 & i2 + 1 <= M + 1 ) by ;
then i2 + 1 in Seg (M + 1) by FINSEQ_1:1;
then A21: [i1,(i2 + 1)] in Indices G by ;
A22: j1 in dom (DelCol (G,i)) by ;
A23: j2 in Seg (width (DelCol (G,i))) by ;
then A24: 1 <= j2 by FINSEQ_1:1;
M <= M + 1 by NAT_1:11;
then A25: Seg (width (DelCol (G,i))) c= Seg () by ;
then A26: [j1,j2] in Indices G by ;
A27: j2 <= M by ;
then ( 1 <= j2 + 1 & j2 + 1 <= M + 1 ) by ;
then j2 + 1 in Seg (M + 1) by FINSEQ_1:1;
then A28: [j1,(j2 + 1)] in Indices G by ;
A29: [i1,i2] in Indices G by ;
now :: thesis: ( ( i2 < i & j2 < i & |.(i1 - j1).| + |.(i2 - j2).| = 1 ) or ( i <= i2 & j2 < i & contradiction ) or ( i2 < i & i <= j2 & contradiction ) or ( i <= i2 & i <= j2 & 1 = |.(i1 - j1).| + |.(i2 - j2).| ) )
per cases ( ( i2 < i & j2 < i ) or ( i <= i2 & j2 < i ) or ( i2 < i & i <= j2 ) or ( i <= i2 & i <= j2 ) ) ;
case ( i2 < i & j2 < i ) ; :: thesis: |.(i1 - j1).| + |.(i2 - j2).| = 1
then ( f /. n = G * (i1,i2) & f /. (n + 1) = G * (j1,j2) ) by A2, A5, A9, A10, A8, A16, A17, A22, A19, A24, Th8;
hence |.(i1 - j1).| + |.(i2 - j2).| = 1 by A1, A13, A29, A26; :: thesis: verum
end;
case A30: ( i <= i2 & j2 < i ) ; :: thesis: contradiction
i2 <= i2 + 1 by NAT_1:11;
then i <= i2 + 1 by ;
then A31: j2 < i2 + 1 by ;
then j2 + 1 <= i2 + 1 by NAT_1:13;
then A32: 1 <= (i2 + 1) - j2 by XREAL_1:19;
( f /. n = G * (i1,(i2 + 1)) & f /. (n + 1) = G * (j1,j2) ) by A2, A5, A9, A8, A16, A17, A22, A20, A24, A30, Th8, Th9;
then A33: 1 = |.(i1 - j1).| + |.((i2 + 1) - j2).| by A1, A13, A26, A21;
0 < (i2 + 1) - j2 by ;
then A34: |.((i2 + 1) - j2).| = (i2 + 1) - j2 by ABSVALUE:def 1;
0 <= |.(i1 - j1).| by COMPLEX1:46;
then 0 + ((i2 + 1) - j2) <= 1 by ;
then (i2 + 1) - j2 = 1 by ;
hence contradiction by A30; :: thesis: verum
end;
case A35: ( i2 < i & i <= j2 ) ; :: thesis: contradiction
j2 <= j2 + 1 by NAT_1:11;
then i <= j2 + 1 by ;
then A36: i2 < j2 + 1 by ;
then i2 + 1 <= j2 + 1 by NAT_1:13;
then A37: 1 <= (j2 + 1) - i2 by XREAL_1:19;
( f /. n = G * (i1,i2) & f /. (n + 1) = G * (j1,(j2 + 1)) ) by A2, A5, A9, A8, A16, A17, A22, A19, A27, A35, Th8, Th9;
then A38: 1 = |.(i1 - j1).| + |.(i2 - (j2 + 1)).| by A1, A13, A29, A28
.= |.(i1 - j1).| + |.(- ((j2 + 1) - i2)).|
.= |.(i1 - j1).| + |.((j2 + 1) - i2).| by COMPLEX1:52 ;
0 < (j2 + 1) - i2 by ;
then A39: |.((j2 + 1) - i2).| = (j2 + 1) - i2 by ABSVALUE:def 1;
0 <= |.(i1 - j1).| by COMPLEX1:46;
then 0 + ((j2 + 1) - i2) <= 1 by ;
then (j2 + 1) - i2 = 1 by ;
hence contradiction by A35; :: thesis: verum
end;
case ( i <= i2 & i <= j2 ) ; :: thesis: 1 = |.(i1 - j1).| + |.(i2 - j2).|
then ( f /. n = G * (i1,(i2 + 1)) & f /. (n + 1) = G * (j1,(j2 + 1)) ) by A2, A5, A9, A10, A8, A16, A17, A22, A20, A27, Th9;
hence 1 = |.(i1 - j1).| + |.((i2 + 1) - (j2 + 1)).| by A1, A13, A21, A28
.= |.(i1 - j1).| + |.(i2 - j2).| ;
:: thesis: verum
end;
end;
end;
hence |.(i1 - j1).| + |.(i2 - j2).| = 1 ; :: thesis: verum
end;
A40: 1 <= i by ;
A41: i <= width G by ;
now :: thesis: for n being Nat st n in dom f holds
ex m, k being Nat st
( [m,k] in Indices (DelCol (G,i)) & f /. n = (DelCol (G,i)) * (m,k) )
let n be Nat; :: thesis: ( n in dom f implies ex m, k being Nat st
( [m,k] in Indices (DelCol (G,i)) & f /. n = (DelCol (G,i)) * (m,k) ) )

assume A42: n in dom f ; :: thesis: ex m, k being Nat st
( [m,k] in Indices (DelCol (G,i)) & f /. n = (DelCol (G,i)) * (m,k) )

then consider m, k being Nat such that
A43: [m,k] in Indices G and
A44: f /. n = G * (m,k) by A1;
take m = m; :: thesis: ex k being Nat st
( [m,k] in Indices (DelCol (G,i)) & f /. n = (DelCol (G,i)) * (m,k) )

A45: m in dom G by ;
A46: k in Seg () by ;
then A47: 1 <= k by FINSEQ_1:1;
A48: k <= M + 1 by ;
now :: thesis: ex k being Nat st
( [m,k] in Indices (DelCol (G,i)) & f /. n = (DelCol (G,i)) * (m,k) )
per cases ( k < i or i <= k ) ;
suppose A49: k < i ; :: thesis: ex k being Nat st
( [m,k] in Indices (DelCol (G,i)) & f /. n = (DelCol (G,i)) * (m,k) )

take k = k; :: thesis: ( [m,k] in Indices (DelCol (G,i)) & f /. n = (DelCol (G,i)) * (m,k) )
k < width G by ;
then k <= M by ;
then k in Seg M by ;
hence ( [m,k] in Indices (DelCol (G,i)) & f /. n = (DelCol (G,i)) * (m,k) ) by A2, A5, A9, A10, A11, A8, A6, A44, A45, A47, A49, Th8, ZFMISC_1:87; :: thesis: verum
end;
suppose i <= k ; :: thesis: ex l being Nat st
( [m,l] in Indices (DelCol (G,i)) & f /. n = (DelCol (G,i)) * (m,l) )

then A50: i < k by ;
then k - 1 in NAT by ;
then reconsider l = k - 1 as Nat ;
take l = l; :: thesis: ( [m,l] in Indices (DelCol (G,i)) & f /. n = (DelCol (G,i)) * (m,l) )
A51: l <= M by ;
i + 1 <= k by ;
then A52: i <= k - 1 by XREAL_1:19;
then 1 <= l by ;
then A53: l in Seg M by ;
(DelCol (G,i)) * (m,l) = G * (m,(l + 1)) by A2, A9, A40, A45, A52, A51, Th9;
hence ( [m,l] in Indices (DelCol (G,i)) & f /. n = (DelCol (G,i)) * (m,l) ) by ; :: thesis: verum
end;
end;
end;
hence ex k being Nat st
( [m,k] in Indices (DelCol (G,i)) & f /. n = (DelCol (G,i)) * (m,k) ) ; :: thesis: verum
end;
hence f is_sequence_on DelCol (G,i) by A12; :: thesis: verum