let G be Go-board; :: thesis:
let f be FinSequence of (TOP-REAL 2); :: thesis:
set D = DelCol G,(width G);
assume A1: ( f is_sequence_on G & f /. 1 in rng (Col G,1) & f /. (len f) in rng (Col G,(width G)) & width G > 1 & 1 <= len f ) ; :: thesis:
then consider k being Element of NAT such that
A2: ( width G = k + 1 & k > 0 ) by Th3;
A3: 0 + 1 <= k by A2, NAT_1:13;
A4: ( width G in Seg (width G) & dom f = dom f ) by A1, FINSEQ_1:3;
then A5: len (DelCol G,(width G)) = len G by A1, Def10;
A6: Indices G = [:(dom G),(Seg (width G)):] by MATRIX_1:def 5;
A7: ( dom G = Seg (len G) & dom (DelCol G,(width G)) = Seg (len (DelCol G,(width G))) & dom f = Seg (len f) ) by FINSEQ_1:def 3;
defpred S₁[ Nat] means ( $1 in dom f & f /. $1 in rng (Col G,k) );
ex m being Element of NAT st S₁[m]

k <= k + 1 by NAT_1:11;
hence ex m being Element of NAT st S₁[m] by A1, A2, A3, Th49; :: thesis:

end;

then A8: ex m being Nat st S₁[m] ;
consider m being Nat such that
A9: ( S₁[m] & ( for i being Nat st S₁[i] holds
m <= i ) ) from NAT_1:sch 5(A8);
A10: for i being Element of NAT st S₁[i] holds
m <= i by A9;
reconsider m = m as Element of NAT by ORDINAL1:def 13;
take t = f | m; :: thesis:
A11: t = f | (Seg m) by FINSEQ_1:def 15;
A12: width (DelCol G,(width G)) = k by A2, A4, Th26;
then ( 1 < width G & width (DelCol G,(width G)) < width G ) by A2, A3, NAT_1:13;
then A13: ( Col (DelCol G,(width G)),1 = Col G,1 & Col (DelCol G,(width G)),(width (DelCol G,(width G))) = Col G,(width (DelCol G,(width G))) ) by A2, A3, A4, A12, Th29;
A14: ( 1 <= m & m <= len f ) by A9, FINSEQ_3:27;
then A15: ( len t = m & dom t = Seg (len t) ) by FINSEQ_1:80, FINSEQ_1:def 3;
then ( 1 in Seg m & len t in Seg m ) by A14, FINSEQ_1:3;
hence ( t /. 1 in rng (Col (DelCol G,(width G)),1) & t /. (len t) in rng (Col (DelCol G,(width G)),(width (DelCol G,(width G)))) & 1 <= len t ) by A1, A9, A12, A13, A15, FINSEQ_1:3, FINSEQ_4:86; :: thesis:
A16: Indices (DelCol G,(width G)) = [:(dom (DelCol G,(width G))),(Seg (width (DelCol G,(width G)))):] by MATRIX_1:def 5;

A17: now

let n be Element of NAT ; :: thesis:
assume A18: n in dom t ; :: thesis:
then A19: ( n in dom f & t /. n = f /. n & n <= m ) by A9, A15, FINSEQ_3:27, FINSEQ_4:86;
then consider i, j being Element of NAT such that
A20: ( [i,j] in Indices G & f /. n = G * i,j ) by A1, Def11;
take i = i; :: thesis:
take j = j; :: thesis:
A21: ( i in dom G & j in Seg (width G) & len (Col G,j) = len G & dom (Col G,j) = Seg (len (Col G,j)) & ( for i being Element of NAT st i in dom G holds
(Col G,j) . i = G * i,j ) ) by A6, A20, FINSEQ_1:def 3, MATRIX_1:def 9, ZFMISC_1:106;
then (Col G,j) . i = G * i,j ;
then A22: ( 1 <= j & f /. n in rng (Col G,j) ) by A7, A20, A21, FINSEQ_1:3, FUNCT_1:def 5;
k <= k + 1 by NAT_1:11;
then k in Seg (width G) by A2, A3, FINSEQ_1:3;
then j <= k by A1, A9, A10, A19, A21, A22, Th50;
then A23: j in Seg k by A22, FINSEQ_1:3;
hence [i,j] in Indices (DelCol G,(width G)) by A5, A7, A12, A16, A21, ZFMISC_1:106; :: thesis:
thus t /. n = G * i,j by A9, A15, A18, A20, FINSEQ_4:86
.= (DelCol G,(width G)) * i,j by A2, A21, A23, Th36 ; :: thesis:

end;

now

let n be Element of NAT ; :: thesis:
assume ( n in dom t & n + 1 in dom t ) ; :: thesis:
then A24: ( t /. n = f /. n & t /. (n + 1) = f /. (n + 1) & n in dom f & n + 1 in dom f ) by A9, A15, FINSEQ_4:86;
let i1, i2, j1, j2 be Element of NAT ; :: thesis:
assume A25: ( [i1,i2] in Indices (DelCol G,(width G)) & [j1,j2] in Indices (DelCol G,(width G)) & t /. n = (DelCol G,(width G)) * i1,i2 & t /. (n + 1) = (DelCol G,(width G)) * j1,j2 ) ; :: thesis:
then A26: ( i1 in dom (DelCol G,(width G)) & i2 in Seg k & j1 in dom (DelCol G,(width G)) & j2 in Seg k ) by A12, A16, ZFMISC_1:106;
then A27: ( f /. n = G * i1,i2 & f /. (n + 1) = G * j1,j2 ) by A2, A5, A7, A24, A25, Th36;
k <= k + 1 by NAT_1:11;
then Seg k c= Seg (width G) by A2, FINSEQ_1:7;
then ( [i1,i2] in Indices G & [j1,j2] in Indices G ) by A5, A6, A7, A26, ZFMISC_1:106;
hence (abs (i1 - j1)) + (abs (i2 - j2)) = 1 by A1, A24, A27, Def11; :: thesis:

end;

hence t is_sequence_on DelCol G,(width G) by A17, Def11; :: thesis:
thus rng t c= rng f by A11, RELAT_1:99; :: thesis: