let i be Element of 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 A2, A4, Def10;
A6: Indices (DelCol G,i) = [:(dom (DelCol G,i)),(Seg (width (DelCol G,i))):] by MATRIX_1:def 5;
A7: Indices G = [:(dom G),(Seg (width G)):] by MATRIX_1:def 5;
A8: ( dom G = Seg (len G) & dom (DelCol G,i) = Seg (len (DelCol G,i)) ) by FINSEQ_1:def 3;
consider M being Element of NAT such that
A9: width G = M + 1 and
A10: M > 0 by A4, SEQM_3:83;
A11: width (DelCol G,i) = M by A2, A9, A10, Th26;

A12: now

let n be Element of NAT ; :: thesis: ( n in dom f & n + 1 in dom f implies for i1, i2, j1, j2 being Element of 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
(abs (i1 - j1)) + (abs (i2 - j2)) = 1 )
assume A13: ( n in dom f & n + 1 in dom f ) ; :: thesis: for i1, i2, j1, j2 being Element of 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
(abs (i1 - j1)) + (abs (i2 - j2)) = 1
let i1, i2, j1, j2 be Element of 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 (abs (i1 - j1)) + (abs (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: (abs (i1 - j1)) + (abs (i2 - j2)) = 1
A17: i1 in dom (DelCol G,i) by A6, A14, ZFMISC_1:106;
A18: i2 in Seg (width (DelCol G,i)) by A6, A14, ZFMISC_1:106;
then A19: 1 <= i2 by FINSEQ_1:3;
A20: i2 <= M by A11, A18, FINSEQ_1:3;
then ( 1 <= i2 + 1 & i2 + 1 <= M + 1 ) by NAT_1:11, XREAL_1:8;
then i2 + 1 in Seg (M + 1) by FINSEQ_1:3;
then A21: [i1,(i2 + 1)] in Indices G by A5, A9, A8, A7, A17, ZFMISC_1:106;
A22: j1 in dom (DelCol G,i) by A6, A15, ZFMISC_1:106;
A23: j2 in Seg (width (DelCol G,i)) by A6, A15, ZFMISC_1:106;
then A24: 1 <= j2 by FINSEQ_1:3;
M <= M + 1 by NAT_1:11;
then A25: Seg (width (DelCol G,i)) c= Seg (width G) by A9, A11, FINSEQ_1:7;
then A26: [j1,j2] in Indices G by A5, A8, A7, A22, A23, ZFMISC_1:106;
A27: j2 <= M by A11, A23, FINSEQ_1:3;
then ( 1 <= j2 + 1 & j2 + 1 <= M + 1 ) by NAT_1:11, XREAL_1:8;
then j2 + 1 in Seg (M + 1) by FINSEQ_1:3;
then A28: [j1,(j2 + 1)] in Indices G by A5, A9, A8, A7, A22, ZFMISC_1:106;
A29: [i1,i2] in Indices G by A5, A8, A7, A17, A18, A25, ZFMISC_1:106;

now

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

end;

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:21;
( f /. n = G * i1,(i2 + 1) & f /. (n + 1) = G * j1,j2 ) by A2, A5, A9, A8, A16, A17, A22, A20, A24, A30, Th31, Th32;
then A33: 1 = (abs (i1 - j1)) + (abs ((i2 + 1) - j2)) by A1, A13, A26, A21, Def11;
0 < (i2 + 1) - j2 by A31, XREAL_1:52;
then A34: abs ((i2 + 1) - j2) = (i2 + 1) - j2 by ABSVALUE:def 1;
0 <= abs (i1 - j1) by COMPLEX1:132;
then 0 + ((i2 + 1) - j2) <= 1 by A33, A34, XREAL_1:9;
then (i2 + 1) - j2 = 1 by A32, XXREAL_0:1;
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 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:21;
( f /. n = G * i1,i2 & f /. (n + 1) = G * j1,(j2 + 1) ) by A2, A5, A9, A8, A16, A17, A22, A19, A27, A35, Th31, Th32;
then A38: 1 = (abs (i1 - j1)) + (abs (i2 - (j2 + 1))) by A1, A13, A29, A28, Def11
.= (abs (i1 - j1)) + (abs (- ((j2 + 1) - i2)))
.= (abs (i1 - j1)) + (abs ((j2 + 1) - i2)) by COMPLEX1:138 ;
0 < (j2 + 1) - i2 by A36, XREAL_1:52;
then A39: abs ((j2 + 1) - i2) = (j2 + 1) - i2 by ABSVALUE:def 1;
0 <= abs (i1 - j1) by COMPLEX1:132;
then 0 + ((j2 + 1) - i2) <= 1 by A38, A39, XREAL_1:9;
then (j2 + 1) - i2 = 1 by A37, XXREAL_0:1;
hence contradiction by A35; :: thesis: verum

end;

case ( i <= i2 & i <= j2 ) ; :: thesis: 1 = (abs (i1 - j1)) + (abs (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, Th32;
hence 1 = (abs (i1 - j1)) + (abs ((i2 + 1) - (j2 + 1))) by A1, A13, A21, A28, Def11
.= (abs (i1 - j1)) + (abs (i2 - j2)) ;
:: thesis: verum

end;

end;

end;

hence (abs (i1 - j1)) + (abs (i2 - j2)) = 1 ; :: thesis: verum

end;

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

now

let n be Element of NAT ; :: thesis: ( n in dom f implies ex m, k being Element of 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 Element of NAT st
( [m,k] in Indices (DelCol G,i) & f /. n = (DelCol G,i) * m,k )
then consider m, k being Element of NAT such that
A43: [m,k] in Indices G and
A44: f /. n = G * m,k by A1, Def11;
take m = m; :: thesis: ex k being Element of 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:106;
A46: k in Seg (width G) by A7, A43, ZFMISC_1:106;
then A47: 1 <= k by FINSEQ_1:3;
A48: k <= M + 1 by A9, A46, FINSEQ_1:3;

now

per cases ( k < i or i <= k ) ;

suppose A49: k < i ; :: thesis: ex k being Element of 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 A41, A49, XXREAL_0:2;
then k <= M by A9, NAT_1:13;
then k in Seg M by A47, FINSEQ_1:3;
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, Th31, ZFMISC_1:106; :: thesis: verum

end;

suppose i <= k ; :: thesis: ex l being Element of NAT st
( [m,l] in Indices (DelCol G,i) & f /. n = (DelCol G,i) * m,l )

then A50: i < k by A3, A42, A44, A45, Th24, XXREAL_0:1;
then reconsider l = k - 1 as Element of NAT by A40, INT_1:18, XXREAL_0:2;
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:22;
i + 1 <= k by A50, NAT_1:13;
then A52: i <= k - 1 by XREAL_1:21;
then 1 <= l by A40, XXREAL_0:2;
then A53: l in Seg M by A51, FINSEQ_1:3;
(DelCol G,i) * m,l = G * m,(l + 1) by A2, A9, A40, A45, A52, A51, Th32;
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:106; :: thesis: verum

end;

end;

end;

hence ex k being Element of 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, Def11; :: thesis: verum