let G be Go-board; :: thesis: for f being FinSequence of (TOP-REAL 2) st 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 holds
ex g being FinSequence of (TOP-REAL 2) st
( g /. 1 in rng (Col (DelCol G,(width G)),1) & g /. (len g) in rng (Col (DelCol G,(width G)),(width (DelCol G,(width G)))) & 1 <= len g & g is_sequence_on DelCol G,(width G) & rng g c= rng f )
let f be FinSequence of (TOP-REAL 2); :: thesis: ( 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 implies ex g being FinSequence of (TOP-REAL 2) st
( g /. 1 in rng (Col (DelCol G,(width G)),1) & g /. (len g) in rng (Col (DelCol G,(width G)),(width (DelCol G,(width G)))) & 1 <= len g & g is_sequence_on DelCol G,(width G) & rng g c= rng f ) )
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: ex g being FinSequence of (TOP-REAL 2) st
( g /. 1 in rng (Col (DelCol G,(width G)),1) & g /. (len g) in rng (Col (DelCol G,(width G)),(width (DelCol G,(width G)))) & 1 <= len g & g is_sequence_on DelCol G,(width G) & rng g c= rng f )
consider k being Element of NAT such that
A6: width G = k + 1 and
A7: k > 0 by A4, SEQM_3:83;
A8: width G in Seg (width G) by A4, FINSEQ_1:3;
then A9: len (DelCol G,(width G)) = len G by A4, Def10;
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, Th29;
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 Element of NAT st S₁[m] by A1, A2, A3, A5, A6, A10, Th49;
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, A7, A8, Th26;
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, Th29;
A17: dom (DelCol G,(width G)) = Seg (len (DelCol G,(width G))) by FINSEQ_1:def 3;
A18: for i being Element of NAT st S₁[i] holds
m <= i by A14;
reconsider m = m as Element of NAT by ORDINAL1:def 13;
A19: 1 <= m by A14, FINSEQ_3:27;
then A20: 1 in Seg m by FINSEQ_1:3;
A21: Indices G = [:(dom G),(Seg (width G)):] by MATRIX_1:def 5;
take t = f | m; :: thesis: ( 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 & t is_sequence_on DelCol G,(width G) & rng t c= rng f )
m <= len f by A14, FINSEQ_3:27;
then A22: len t = m by FINSEQ_1:80;
then len t in Seg m by A19, 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 A2, A14, A15, A11, A16, A22, A20, FINSEQ_1:3, FINSEQ_4:86; :: thesis: ( t is_sequence_on DelCol G,(width G) & rng t c= rng f )
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_1:def 5;

A25: now

k <= k + 1 by NAT_1:11;
then A26: k in Seg (width G) by A6, A10, FINSEQ_1:3;
let n be Element of NAT ; :: thesis: ( n in dom t implies ex i, j being Element of NAT st
( [i,j] in Indices (DelCol G,(width G)) & t /. n = (DelCol G,(width G)) * i,j ) )
assume A27: n in dom t ; :: thesis: ex i, j being Element of NAT st
( [i,j] in Indices (DelCol G,(width G)) & t /. n = (DelCol G,(width G)) * i,j )
then A28: n <= m by A22, FINSEQ_3:27;
A29: n in dom f by A14, A22, A23, A27, FINSEQ_4:86;
then consider i, j being Element of NAT such that
A30: [i,j] in Indices G and
A31: f /. n = G * i,j by A1, Def11;
A32: j in Seg (width G) by A21, A30, ZFMISC_1:106;
then A33: 1 <= j by FINSEQ_1:3;
take i = i; :: thesis: ex j being Element of NAT st
( [i,j] in Indices (DelCol G,(width G)) & t /. n = (DelCol G,(width G)) * i,j )
take j = j; :: thesis: ( [i,j] in Indices (DelCol G,(width G)) & t /. n = (DelCol G,(width G)) * i,j )
A34: ( len (Col G,j) = len G & dom (Col G,j) = Seg (len (Col G,j)) ) by FINSEQ_1:def 3, MATRIX_1:def 9;
A35: i in dom G by A21, A30, ZFMISC_1:106;
then (Col G,j) . i = G * i,j by MATRIX_1:def 9;
then f /. n in rng (Col G,j) by A12, A31, A35, A34, FUNCT_1:def 5;
then j <= k by A1, A2, A18, A29, A28, A32, A26, Th50;
then A36: j in Seg k by A33, FINSEQ_1:3;
hence [i,j] in Indices (DelCol G,(width G)) by A9, A12, A17, A15, A24, A35, ZFMISC_1:106; :: thesis: t /. n = (DelCol G,(width G)) * i,j
thus t /. n = G * i,j by A14, A22, A23, A27, A31, FINSEQ_4:86
.= (DelCol G,(width G)) * i,j by A6, A7, A35, A36, Th36 ; :: thesis: verum

end;

now

let n be Element of NAT ; :: thesis: ( n in dom t & n + 1 in dom t implies for i1, i2, j1, j2 being Element of NAT st [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 holds
(abs (i1 - j1)) + (abs (i2 - j2)) = 1 )
assume that
A37: n in dom t and
A38: n + 1 in dom t ; :: thesis: for i1, i2, j1, j2 being Element of NAT st [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 holds
(abs (i1 - j1)) + (abs (i2 - j2)) = 1
A39: ( n in dom f & n + 1 in dom f ) by A14, A22, A23, A37, A38, FINSEQ_4:86;
let i1, i2, j1, j2 be Element of NAT ; :: thesis: ( [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 implies (abs (i1 - j1)) + (abs (i2 - j2)) = 1 )
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: (abs (i1 - j1)) + (abs (i2 - j2)) = 1
A44: ( i1 in dom (DelCol G,(width G)) & i2 in Seg k ) by A15, A24, A40, ZFMISC_1:106;
A45: ( j1 in dom (DelCol G,(width G)) & j2 in Seg k ) by A15, A24, A41, ZFMISC_1:106;
t /. n = f /. n by A14, A22, A23, A37, FINSEQ_4:86;
then A46: f /. n = G * i1,i2 by A6, A7, A9, A12, A17, A42, A44, Th36;
k <= k + 1 by NAT_1:11;
then A47: Seg k c= Seg (width G) by A6, FINSEQ_1:7;
then A48: [j1,j2] in Indices G by A9, A21, A12, A17, A45, ZFMISC_1:106;
t /. (n + 1) = f /. (n + 1) by A14, A22, A23, A38, FINSEQ_4:86;
then A49: f /. (n + 1) = G * j1,j2 by A6, A7, A9, A12, A17, A43, A45, Th36;
[i1,i2] in Indices G by A9, A21, A12, A17, A44, A47, ZFMISC_1:106;
hence (abs (i1 - j1)) + (abs (i2 - j2)) = 1 by A1, A39, A46, A49, A48, Def11; :: thesis: verum

end;

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