let i be Nat; :: thesis: for G being Go-board

for f being FinSequence of (TOP-REAL 2) st f is_sequence_on G & i in Seg (width G) & 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 (TOP-REAL 2) st f is_sequence_on G & i in Seg (width G) & rng f misses rng (Col (G,i)) & width G > 1 holds

f is_sequence_on DelCol (G,i)

let f be FinSequence of (TOP-REAL 2); :: thesis: ( f is_sequence_on G & i in Seg (width G) & 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 (width G) 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 (width G)):] 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 A4, SEQM_3:43;

A11: width (DelCol (G,i)) = M by A2, A9, MATRIX_0:63;

A41: i <= width G by A2, FINSEQ_1:1;

for f being FinSequence of (TOP-REAL 2) st f is_sequence_on G & i in Seg (width G) & 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 (TOP-REAL 2) st f is_sequence_on G & i in Seg (width G) & rng f misses rng (Col (G,i)) & width G > 1 holds

f is_sequence_on DelCol (G,i)

let f be FinSequence of (TOP-REAL 2); :: thesis: ( f is_sequence_on G & i in Seg (width G) & 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 (width G) 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 (width G)):] 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 A4, SEQM_3:43;

A11: width (DelCol (G,i)) = M by A2, A9, MATRIX_0:63;

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

A40:
1 <= i
by A2, FINSEQ_1:1;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 A6, A14, ZFMISC_1:87;

A18: i2 in Seg (width (DelCol (G,i))) by A6, A14, ZFMISC_1:87;

then A19: 1 <= i2 by FINSEQ_1:1;

A20: i2 <= M by A11, A18, FINSEQ_1:1;

then ( 1 <= i2 + 1 & i2 + 1 <= M + 1 ) by NAT_1:11, XREAL_1:6;

then i2 + 1 in Seg (M + 1) by FINSEQ_1:1;

then A21: [i1,(i2 + 1)] in Indices G by A5, A9, A8, A7, A17, ZFMISC_1:87;

A22: j1 in dom (DelCol (G,i)) by A6, A15, ZFMISC_1:87;

A23: j2 in Seg (width (DelCol (G,i))) by A6, A15, ZFMISC_1:87;

then A24: 1 <= j2 by FINSEQ_1:1;

M <= M + 1 by NAT_1:11;

then A25: Seg (width (DelCol (G,i))) c= Seg (width G) by A9, A11, FINSEQ_1:5;

then A26: [j1,j2] in Indices G by A5, A8, A7, A22, A23, ZFMISC_1:87;

A27: j2 <= M by A11, A23, FINSEQ_1:1;

then ( 1 <= j2 + 1 & j2 + 1 <= M + 1 ) by NAT_1:11, XREAL_1:6;

then j2 + 1 in Seg (M + 1) by FINSEQ_1:1;

then A28: [j1,(j2 + 1)] in Indices G by A5, A9, A8, A7, A22, ZFMISC_1:87;

A29: [i1,i2] in Indices G by A5, A8, A7, A17, A18, A25, ZFMISC_1:87;

end;|.(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 A6, A14, ZFMISC_1:87;

A18: i2 in Seg (width (DelCol (G,i))) by A6, A14, ZFMISC_1:87;

then A19: 1 <= i2 by FINSEQ_1:1;

A20: i2 <= M by A11, A18, FINSEQ_1:1;

then ( 1 <= i2 + 1 & i2 + 1 <= M + 1 ) by NAT_1:11, XREAL_1:6;

then i2 + 1 in Seg (M + 1) by FINSEQ_1:1;

then A21: [i1,(i2 + 1)] in Indices G by A5, A9, A8, A7, A17, ZFMISC_1:87;

A22: j1 in dom (DelCol (G,i)) by A6, A15, ZFMISC_1:87;

A23: j2 in Seg (width (DelCol (G,i))) by A6, A15, ZFMISC_1:87;

then A24: 1 <= j2 by FINSEQ_1:1;

M <= M + 1 by NAT_1:11;

then A25: Seg (width (DelCol (G,i))) c= Seg (width G) by A9, A11, FINSEQ_1:5;

then A26: [j1,j2] in Indices G by A5, A8, A7, A22, A23, ZFMISC_1:87;

A27: j2 <= M by A11, A23, FINSEQ_1:1;

then ( 1 <= j2 + 1 & j2 + 1 <= M + 1 ) by NAT_1:11, XREAL_1:6;

then j2 + 1 in Seg (M + 1) by FINSEQ_1:1;

then A28: [j1,(j2 + 1)] in Indices G by A5, A9, A8, A7, A22, ZFMISC_1:87;

A29: [i1,i2] in Indices G by A5, A8, A7, A17, A18, A25, ZFMISC_1:87;

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).| ) )end;

hence
|.(i1 - j1).| + |.(i2 - j2).| = 1
; :: thesis: verumper cases
( ( i2 < i & j2 < i ) or ( i <= i2 & j2 < i ) or ( i2 < i & i <= j2 ) or ( i <= i2 & i <= j2 ) )
;

end;

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;hence |.(i1 - j1).| + |.(i2 - j2).| = 1 by A1, A13, A29, A26; :: thesis: verum

case A30:
( i <= i2 & j2 < i )
; :: thesis: contradiction

i2 <= i2 + 1
by NAT_1:11;

then i <= i2 + 1 by A30, XXREAL_0:2;

then A31: j2 < i2 + 1 by A30, XXREAL_0:2;

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 A31, XREAL_1:50;

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 A33, A34, XREAL_1:7;

then (i2 + 1) - j2 = 1 by A32, XXREAL_0:1;

hence contradiction by A30; :: thesis: verum

end;then i <= i2 + 1 by A30, XXREAL_0:2;

then A31: j2 < i2 + 1 by A30, XXREAL_0:2;

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 A31, XREAL_1:50;

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 A33, A34, XREAL_1:7;

then (i2 + 1) - j2 = 1 by A32, XXREAL_0:1;

hence contradiction by A30; :: thesis: verum

case A35:
( i2 < i & i <= j2 )
; :: thesis: contradiction

j2 <= j2 + 1
by NAT_1:11;

then i <= j2 + 1 by A35, XXREAL_0:2;

then A36: i2 < j2 + 1 by A35, XXREAL_0:2;

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 A36, XREAL_1:50;

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 A38, A39, XREAL_1:7;

then (j2 + 1) - i2 = 1 by A37, XXREAL_0:1;

hence contradiction by A35; :: thesis: verum

end;then i <= j2 + 1 by A35, XXREAL_0:2;

then A36: i2 < j2 + 1 by A35, XXREAL_0:2;

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 A36, XREAL_1:50;

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 A38, A39, XREAL_1:7;

then (j2 + 1) - i2 = 1 by A37, XXREAL_0:1;

hence contradiction by A35; :: thesis: verum

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;hence 1 = |.(i1 - j1).| + |.((i2 + 1) - (j2 + 1)).| by A1, A13, A21, A28

.= |.(i1 - j1).| + |.(i2 - j2).| ;

:: thesis: verum

A41: i <= width G by A2, FINSEQ_1:1;

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) )

hence
f is_sequence_on DelCol (G,i)
by A12; :: thesis: verumex 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 A7, A43, ZFMISC_1:87;

A46: k in Seg (width G) by A7, A43, ZFMISC_1:87;

then A47: 1 <= k by FINSEQ_1:1;

A48: k <= M + 1 by A9, A46, FINSEQ_1:1;

( [m,k] in Indices (DelCol (G,i)) & f /. n = (DelCol (G,i)) * (m,k) ) ; :: thesis: verum

end;( [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 A7, A43, ZFMISC_1:87;

A46: k in Seg (width G) by A7, A43, ZFMISC_1:87;

then A47: 1 <= k by FINSEQ_1:1;

A48: k <= M + 1 by A9, A46, FINSEQ_1:1;

now :: thesis: ex k being Nat st

( [m,k] in Indices (DelCol (G,i)) & f /. n = (DelCol (G,i)) * (m,k) )end;

hence
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 )
;

end;

suppose A49:
k < i
; :: thesis: ex k being Nat st

( [m,k] in Indices (DelCol (G,i)) & f /. n = (DelCol (G,i)) * (m,k) )

( [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 A41, A49, XXREAL_0:2;

then k <= M by A9, NAT_1:13;

then k in Seg M by A47, FINSEQ_1:1;

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;k < width G by A41, A49, XXREAL_0:2;

then k <= M by A9, NAT_1:13;

then k in Seg M by A47, FINSEQ_1:1;

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

suppose
i <= k
; :: thesis: ex l being Nat st

( [m,l] in Indices (DelCol (G,i)) & f /. n = (DelCol (G,i)) * (m,l) )

( [m,l] in Indices (DelCol (G,i)) & f /. n = (DelCol (G,i)) * (m,l) )

then A50:
i < k
by A3, A42, A44, A45, MATRIX_0:43, XXREAL_0:1;

then k - 1 in NAT by A40, INT_1:5, XXREAL_0:2;

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 A48, XREAL_1:20;

i + 1 <= k by A50, NAT_1:13;

then A52: i <= k - 1 by XREAL_1:19;

then 1 <= l by A40, XXREAL_0:2;

then A53: l in Seg M by A51, FINSEQ_1:1;

(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 A5, A11, A8, A6, A44, A45, A53, ZFMISC_1:87; :: thesis: verum

end;then k - 1 in NAT by A40, INT_1:5, XXREAL_0:2;

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 A48, XREAL_1:20;

i + 1 <= k by A50, NAT_1:13;

then A52: i <= k - 1 by XREAL_1:19;

then 1 <= l by A40, XXREAL_0:2;

then A53: l in Seg M by A51, FINSEQ_1:1;

(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 A5, A11, A8, A6, A44, A45, A53, ZFMISC_1:87; :: thesis: verum

( [m,k] in Indices (DelCol (G,i)) & f /. n = (DelCol (G,i)) * (m,k) ) ; :: thesis: verum