let G be Go-board; :: thesis:
let f be FinSequence of (TOP-REAL 2); :: thesis:
set D = DelCol (G,(width G));
assume that
A1: f is_sequence_on G and
A2: f /. 1 in rng (Col (G,1)) and
A3: f /. (len f) in rng (Col (G,(width G))) and
A4: width G > 1 and
A5: 1 <= len f ; :: thesis:
consider k being Nat such that
A6: width G = k + 1 and
A7: k > 0 by A4, SEQM_3:43;
A8: width G in Seg (width G) by A4, FINSEQ_1:1;
A9: len (DelCol (G,(width G))) = len G by MATRIX_0:def 13;
A10: 0 + 1 <= k by A7, NAT_1:13;
then 1 < width G by A6, NAT_1:13;
then A11: Col ((DelCol (G,(width G))),1) = Col (G,1) by A6, A7, A8, Th6;
A12: dom G = Seg (len G) by FINSEQ_1:def 3;
defpred S₁[ Nat] means ( $1 in dom f & f /. $1 in rng (Col (G,k)) );
k <= k + 1 by NAT_1:11;
then ex m being Nat st S₁[m] by A1, A2, A3, A5, A6, A10, Th26;
then A13: ex m being Nat st S₁[m] ;
consider m being Nat such that
A14: ( S₁[m] & ( for i being Nat st S₁[i] holds
m <= i ) ) from NAT_1:sch 5(A13);
A15: width (DelCol (G,(width G))) = k by A6, A8, MATRIX_0:63;
then width (DelCol (G,(width G))) < width G by A6, NAT_1:13;
then A16: Col ((DelCol (G,(width G))),(width (DelCol (G,(width G))))) = Col (G,(width (DelCol (G,(width G))))) by A6, A10, A8, A15, Th6;
A17: dom (DelCol (G,(width G))) = Seg (len (DelCol (G,(width G)))) by FINSEQ_1:def 3;
A18: for i being Nat st S₁[i] holds
m <= i by A14;
reconsider m = m as Element of NAT by ORDINAL1:def 12;
A19: 1 <= m by A14, FINSEQ_3:25;
then A20: 1 in Seg m by FINSEQ_1:1;
A21: Indices G = [:(dom G),(Seg (width G)):] by MATRIX_0:def 4;
take t = f | m; :: thesis:
m <= len f by A14, FINSEQ_3:25;
then A22: len t = m by FINSEQ_1:59;
then len t in Seg m by A19, FINSEQ_1:1;
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 A2, A14, A15, A11, A16, A22, A20, FINSEQ_1:1, FINSEQ_4:71; :: thesis:
A23: dom t = Seg (len t) by FINSEQ_1:def 3;
A24: Indices (DelCol (G,(width G))) = [:(dom (DelCol (G,(width G)))),(Seg (width (DelCol (G,(width G))))):] by MATRIX_0:def 4;

A25: now :: thesis:

k <= k + 1 by NAT_1:11;
then A26: k in Seg (width G) by A6, A10, FINSEQ_1:1;
let n be Nat; :: thesis:
assume A27: n in dom t ; :: thesis:
then A28: n <= m by A22, FINSEQ_3:25;
A29: n in dom f by A14, A22, A23, A27, FINSEQ_4:71;
then consider i, j being Nat such that
A30: [i,j] in Indices G and
A31: f /. n = G * (i,j) by A1;
A32: j in Seg (width G) by A21, A30, ZFMISC_1:87;
then A33: 1 <= j by FINSEQ_1:1;
take i = i; :: thesis:
take j = j; :: thesis:
A34: ( len (Col (G,j)) = len G & dom (Col (G,j)) = Seg (len (Col (G,j))) ) by FINSEQ_1:def 3, MATRIX_0:def 8;
A35: i in dom G by A21, A30, ZFMISC_1:87;
then (Col (G,j)) . i = G * (i,j) by MATRIX_0:def 8;
then f /. n in rng (Col (G,j)) by A12, A31, A35, A34, FUNCT_1:def 3;
then j <= k by A1, A2, A18, A29, A28, A32, A26, Th27;
then A36: j in Seg k by A33, FINSEQ_1:1;
hence [i,j] in Indices (DelCol (G,(width G))) by A9, A12, A17, A15, A24, A35, ZFMISC_1:87; :: thesis:
thus t /. n = G * (i,j) by A14, A22, A23, A27, A31, FINSEQ_4:71
.= (DelCol (G,(width G))) * (i,j) by A6, A7, A35, A36, Th13 ; :: thesis:

end;

let n be Nat; :: thesis:
assume that
A37: n in dom t and
A38: n + 1 in dom t ; :: thesis:
A39: ( n in dom f & n + 1 in dom f ) by A14, A22, A23, A37, A38, FINSEQ_4:71;
let i1, i2, j1, j2 be Nat; :: thesis:
assume that
A40: [i1,i2] in Indices (DelCol (G,(width G))) and
A41: [j1,j2] in Indices (DelCol (G,(width G))) and
A42: t /. n = (DelCol (G,(width G))) * (i1,i2) and
A43: t /. (n + 1) = (DelCol (G,(width G))) * (j1,j2) ; :: thesis:
A44: ( i1 in dom (DelCol (G,(width G))) & i2 in Seg k ) by A15, A24, A40, ZFMISC_1:87;
A45: ( j1 in dom (DelCol (G,(width G))) & j2 in Seg k ) by A15, A24, A41, ZFMISC_1:87;
t /. n = f /. n by A14, A22, A23, A37, FINSEQ_4:71;
then A46: f /. n = G * (i1,i2) by A6, A7, A9, A12, A17, A42, A44, Th13;
k <= k + 1 by NAT_1:11;
then A47: Seg k c= Seg (width G) by A6, FINSEQ_1:5;
then A48: [j1,j2] in Indices G by A9, A21, A12, A17, A45, ZFMISC_1:87;
t /. (n + 1) = f /. (n + 1) by A14, A22, A23, A38, FINSEQ_4:71;
then A49: f /. (n + 1) = G * (j1,j2) by A6, A7, A9, A12, A17, A43, A45, Th13;
[i1,i2] in Indices G by A9, A21, A12, A17, A44, A47, ZFMISC_1:87;
hence |.(i1 - j1).| + |.(i2 - j2).| = 1 by A1, A39, A46, A49, A48; :: thesis:

end;

hence t is_sequence_on DelCol (G,(width G)) by A25; :: thesis:
t = f | (Seg m) by FINSEQ_1:def 15;
hence rng t c= rng f by RELAT_1:70; :: thesis: