let G be Go-board; :: thesis: for f being FinSequence of () st f is_sequence_on G & (rng f) /\ (rng (Col (G,1))) <> {} & (rng f) /\ (rng (Col (G,()))) <> {} holds
ex g being FinSequence of () st
( rng g c= rng f & g /. 1 in rng (Col (G,1)) & g /. (len g) in rng (Col (G,())) & 1 <= len g & g is_sequence_on G )

let f be FinSequence of (); :: thesis: ( f is_sequence_on G & (rng f) /\ (rng (Col (G,1))) <> {} & (rng f) /\ (rng (Col (G,()))) <> {} implies ex g being FinSequence of () st
( rng g c= rng f & g /. 1 in rng (Col (G,1)) & g /. (len g) in rng (Col (G,())) & 1 <= len g & g is_sequence_on G ) )

assume that
A1: f is_sequence_on G and
A2: (rng f) /\ (rng (Col (G,1))) <> {} and
A3: (rng f) /\ (rng (Col (G,()))) <> {} ; :: thesis: ex g being FinSequence of () st
( rng g c= rng f & g /. 1 in rng (Col (G,1)) & g /. (len g) in rng (Col (G,())) & 1 <= len g & g is_sequence_on G )

set y = the Element of (rng f) /\ (rng (Col (G,())));
set x = the Element of (rng f) /\ (rng (Col (G,1)));
A4: ( the Element of (rng f) /\ (rng (Col (G,1))) in rng (Col (G,1)) & the Element of (rng f) /\ (rng (Col (G,()))) in rng (Col (G,())) ) by ;
the Element of (rng f) /\ (rng (Col (G,()))) in rng f by ;
then consider m being Element of NAT such that
A5: m in dom f and
A6: the Element of (rng f) /\ (rng (Col (G,()))) = f /. m by PARTFUN2:2;
A7: 1 <= m by ;
A8: the Element of (rng f) /\ (rng (Col (G,1))) in rng f by ;
then consider n being Element of NAT such that
A9: n in dom f and
A10: the Element of (rng f) /\ (rng (Col (G,1))) = f /. n by PARTFUN2:2;
reconsider x = the Element of (rng f) /\ (rng (Col (G,1))) as Point of () by A10;
A11: 1 <= n by ;
per cases ( n = m or n > m or n < m ) by XXREAL_0:1;
suppose A12: n = m ; :: thesis: ex g being FinSequence of () st
( rng g c= rng f & g /. 1 in rng (Col (G,1)) & g /. (len g) in rng (Col (G,())) & 1 <= len g & g is_sequence_on G )

reconsider h = <*x*> as FinSequence of () ;
A13: len h = 1 by FINSEQ_1:39;
A14: now :: thesis: for k being Nat st k in Seg 1 holds
h /. k = x
let k be Nat; :: thesis: ( k in Seg 1 implies h /. k = x )
assume A15: k in Seg 1 ; :: thesis: h /. k = x
then A16: k = 1 by ;
k in dom h by ;
hence h /. k = h . k by PARTFUN1:def 6
.= x by ;
:: thesis: verum
end;
A17: rng h c= rng f
proof
let z be object ; :: according to TARSKI:def 3 :: thesis: ( not z in rng h or z in rng f )
assume z in rng h ; :: thesis: z in rng f
then consider i being Element of NAT such that
A18: i in dom h and
A19: z = h /. i by PARTFUN2:2;
i in Seg 1 by ;
hence z in rng f by A8, A14, A19; :: thesis: verum
end;
reconsider h = h as FinSequence of () ;
take h ; :: thesis: ( rng h c= rng f & h /. 1 in rng (Col (G,1)) & h /. (len h) in rng (Col (G,())) & 1 <= len h & h is_sequence_on G )
thus rng h c= rng f by A17; :: thesis: ( h /. 1 in rng (Col (G,1)) & h /. (len h) in rng (Col (G,())) & 1 <= len h & h is_sequence_on G )
1 in Seg 1 by FINSEQ_1:1;
hence ( h /. 1 in rng (Col (G,1)) & h /. (len h) in rng (Col (G,())) ) by A10, A4, A6, A12, A13, A14; :: thesis: ( 1 <= len h & h is_sequence_on G )
A20: dom h = Seg (len h) by FINSEQ_1:def 3;
A21: now :: thesis: for i being Nat st i in dom h & i + 1 in dom h holds
for i1, i2, j1, j2 being Nat st [i1,i2] in Indices G & [j1,j2] in Indices G & h /. i = G * (i1,i2) & h /. (i + 1) = G * (j1,j2) holds
|.(i1 - j1).| + |.(i2 - j2).| = 1
let i be Nat; :: thesis: ( i in dom h & i + 1 in dom h implies for i1, i2, j1, j2 being Nat st [i1,i2] in Indices G & [j1,j2] in Indices G & h /. i = G * (i1,i2) & h /. (i + 1) = G * (j1,j2) holds
|.(i1 - j1).| + |.(i2 - j2).| = 1 )

assume that
A22: i in dom h and
A23: i + 1 in dom h ; :: thesis: for i1, i2, j1, j2 being Nat st [i1,i2] in Indices G & [j1,j2] in Indices G & h /. i = G * (i1,i2) & h /. (i + 1) = G * (j1,j2) holds
|.(i1 - j1).| + |.(i2 - j2).| = 1

i = 1 by ;
hence for i1, i2, j1, j2 being Nat st [i1,i2] in Indices G & [j1,j2] in Indices G & h /. i = G * (i1,i2) & h /. (i + 1) = G * (j1,j2) holds
|.(i1 - j1).| + |.(i2 - j2).| = 1 by ; :: thesis: verum
end;
now :: thesis: for i being Nat st i in dom h holds
ex i1, i2 being Nat st
( [i1,i2] in Indices G & h /. i = G * (i1,i2) )
consider i1, i2 being Nat such that
A24: ( [i1,i2] in Indices G & f /. n = G * (i1,i2) ) by A1, A9;
let i be Nat; :: thesis: ( i in dom h implies ex i1, i2 being Nat st
( [i1,i2] in Indices G & h /. i = G * (i1,i2) ) )

assume A25: i in dom h ; :: thesis: ex i1, i2 being Nat st
( [i1,i2] in Indices G & h /. i = G * (i1,i2) )

take i1 = i1; :: thesis: ex i2 being Nat st
( [i1,i2] in Indices G & h /. i = G * (i1,i2) )

take i2 = i2; :: thesis: ( [i1,i2] in Indices G & h /. i = G * (i1,i2) )
thus ( [i1,i2] in Indices G & h /. i = G * (i1,i2) ) by A10, A13, A14, A20, A25, A24; :: thesis: verum
end;
hence ( 1 <= len h & h is_sequence_on G ) by ; :: thesis: verum
end;
suppose A26: n > m ; :: thesis: ex g being FinSequence of () st
( rng g c= rng f & g /. 1 in rng (Col (G,1)) & g /. (len g) in rng (Col (G,())) & 1 <= len g & g is_sequence_on G )

n <= n + 1 by NAT_1:11;
then reconsider l = (n + 1) - m as Element of NAT by ;
set f1 = f | n;
defpred S1[ Nat, set ] means for k being Nat st \$1 + k = n + 1 holds
\$2 = (f | n) /. k;
A27: n in Seg n by ;
A28: now :: thesis: for i being Nat st i in Seg l holds
(n + 1) - i is Element of NAT
let i be Nat; :: thesis: ( i in Seg l implies (n + 1) - i is Element of NAT )
assume i in Seg l ; :: thesis: (n + 1) - i is Element of NAT
then A29: i <= l by FINSEQ_1:1;
l <= (n + 1) - 0 by XREAL_1:13;
hence (n + 1) - i is Element of NAT by ; :: thesis: verum
end;
A30: for i being Nat st i in Seg l holds
ex p being Point of () st S1[i,p]
proof
let i be Nat; :: thesis: ( i in Seg l implies ex p being Point of () st S1[i,p] )
assume i in Seg l ; :: thesis: ex p being Point of () st S1[i,p]
then reconsider a = (n + 1) - i as Element of NAT by A28;
take (f | n) /. a ; :: thesis: S1[i,(f | n) /. a]
let k be Nat; :: thesis: ( i + k = n + 1 implies (f | n) /. a = (f | n) /. k )
assume i + k = n + 1 ; :: thesis: (f | n) /. a = (f | n) /. k
hence (f | n) /. a = (f | n) /. k ; :: thesis: verum
end;
consider g being FinSequence of () such that
A31: ( len g = l & ( for i being Nat st i in Seg l holds
S1[i,g /. i] ) ) from take g ; :: thesis: ( rng g c= rng f & g /. 1 in rng (Col (G,1)) & g /. (len g) in rng (Col (G,())) & 1 <= len g & g is_sequence_on G )
A32: dom g = Seg (len g) by FINSEQ_1:def 3;
A33: for i being Nat st i in Seg l holds
( (n + 1) - i is Element of NAT & (f | n) /. ((n + 1) - i) = f /. ((n + 1) - i) & (n + 1) - i in dom f )
proof
let i be Nat; :: thesis: ( i in Seg l implies ( (n + 1) - i is Element of NAT & (f | n) /. ((n + 1) - i) = f /. ((n + 1) - i) & (n + 1) - i in dom f ) )
assume A34: i in Seg l ; :: thesis: ( (n + 1) - i is Element of NAT & (f | n) /. ((n + 1) - i) = f /. ((n + 1) - i) & (n + 1) - i in dom f )
then A35: i <= l by FINSEQ_1:1;
l <= (n + 1) - 0 by XREAL_1:13;
then reconsider w = (n + 1) - i as Element of NAT by ;
1 <= i by ;
then A36: (n + 1) - i <= (n + 1) - 1 by XREAL_1:13;
(n + 1) - l <= (n + 1) - i by ;
then 1 <= (n + 1) - i by ;
then w in Seg n by ;
hence ( (n + 1) - i is Element of NAT & (f | n) /. ((n + 1) - i) = f /. ((n + 1) - i) & (n + 1) - i in dom f ) by ; :: thesis: verum
end;
thus rng g c= rng f :: thesis: ( g /. 1 in rng (Col (G,1)) & g /. (len g) in rng (Col (G,())) & 1 <= len g & g is_sequence_on G )
proof
let z be object ; :: according to TARSKI:def 3 :: thesis: ( not z in rng g or z in rng f )
assume z in rng g ; :: thesis: z in rng f
then consider i being Element of NAT such that
A37: i in dom g and
A38: z = g /. i by PARTFUN2:2;
reconsider yy = (n + 1) - i as Element of NAT by A28, A31, A32, A37;
i + yy = n + 1 ;
then A39: z = (f | n) /. yy by A31, A32, A37, A38;
( (f | n) /. yy = f /. yy & yy in dom f ) by A33, A31, A32, A37;
hence z in rng f by ; :: thesis: verum
end;
A40: dom g = Seg (len g) by FINSEQ_1:def 3;
A41: now :: thesis: for i being Nat st i in dom g & i + 1 in dom g holds
for i1, i2, j1, j2 being Nat st [i1,i2] in Indices G & [j1,j2] in Indices G & g /. i = G * (i1,i2) & g /. (i + 1) = G * (j1,j2) holds
1 = |.(i1 - j1).| + |.(i2 - j2).|
let i be Nat; :: thesis: ( i in dom g & i + 1 in dom g implies for i1, i2, j1, j2 being Nat st [i1,i2] in Indices G & [j1,j2] in Indices G & g /. i = G * (i1,i2) & g /. (i + 1) = G * (j1,j2) holds
1 = |.(i1 - j1).| + |.(i2 - j2).| )

assume that
A42: i in dom g and
A43: i + 1 in dom g ; :: thesis: for i1, i2, j1, j2 being Nat st [i1,i2] in Indices G & [j1,j2] in Indices G & g /. i = G * (i1,i2) & g /. (i + 1) = G * (j1,j2) holds
1 = |.(i1 - j1).| + |.(i2 - j2).|

let i1, i2, j1, j2 be Nat; :: thesis: ( [i1,i2] in Indices G & [j1,j2] in Indices G & g /. i = G * (i1,i2) & g /. (i + 1) = G * (j1,j2) implies 1 = |.(i1 - j1).| + |.(i2 - j2).| )
assume A44: ( [i1,i2] in Indices G & [j1,j2] in Indices G & g /. i = G * (i1,i2) & g /. (i + 1) = G * (j1,j2) ) ; :: thesis: 1 = |.(i1 - j1).| + |.(i2 - j2).|
reconsider xx = (n + 1) - (i + 1) as Element of NAT by A28, A31, A40, A43;
(i + 1) + xx = n + 1 ;
then g /. (i + 1) = (f | n) /. xx by ;
then A45: g /. (i + 1) = f /. xx by A33, A31, A32, A43;
A46: xx + 1 = (n + 1) - i ;
reconsider ww = (n + 1) - i as Element of NAT by A28, A31, A40, A42;
i + ww = n + 1 ;
then g /. i = (f | n) /. ww by ;
then A47: g /. i = f /. ww by A33, A31, A32, A42;
( ww in dom f & xx in dom f ) by A33, A31, A32, A42, A43;
hence 1 = |.(j1 - i1).| + |.(j2 - i2).| by A1, A47, A45, A46, A44
.= |.(- (i1 - j1)).| + |.(- (i2 - j2)).|
.= |.(i1 - j1).| + |.(- (i2 - j2)).| by COMPLEX1:52
.= |.(i1 - j1).| + |.(i2 - j2).| by COMPLEX1:52 ;
:: thesis: verum
end;
m + 1 <= n by ;
then A48: m + 1 <= n + 1 by NAT_1:13;
then A49: 1 <= l by XREAL_1:19;
then 1 in Seg l by FINSEQ_1:1;
then g /. 1 = (f | n) /. n by A31
.= f /. n by ;
hence g /. 1 in rng (Col (G,1)) by ; :: thesis: ( g /. (len g) in rng (Col (G,())) & 1 <= len g & g is_sequence_on G )
A50: m in Seg n by ;
reconsider ww = (n + 1) - l as Element of NAT ;
A51: l + ww = n + 1 ;
len g in dom g by ;
then g /. (len g) = (f | n) /. ww by
.= f /. m by ;
hence g /. (len g) in rng (Col (G,())) by ; :: thesis: ( 1 <= len g & g is_sequence_on G )
now :: thesis: for i being Nat st i in dom g holds
ex i1, i2 being Nat st
( [i1,i2] in Indices G & g /. i = G * (i1,i2) )
let i be Nat; :: thesis: ( i in dom g implies ex i1, i2 being Nat st
( [i1,i2] in Indices G & g /. i = G * (i1,i2) ) )

assume A52: i in dom g ; :: thesis: ex i1, i2 being Nat st
( [i1,i2] in Indices G & g /. i = G * (i1,i2) )

then reconsider ww = (n + 1) - i as Element of NAT by ;
ww in dom f by A33, A31, A32, A52;
then consider i1, i2 being Nat such that
A53: ( [i1,i2] in Indices G & f /. ww = G * (i1,i2) ) by A1;
take i1 = i1; :: thesis: ex i2 being Nat st
( [i1,i2] in Indices G & g /. i = G * (i1,i2) )

take i2 = i2; :: thesis: ( [i1,i2] in Indices G & g /. i = G * (i1,i2) )
i + ww = n + 1 ;
then g /. i = (f | n) /. ww by ;
hence ( [i1,i2] in Indices G & g /. i = G * (i1,i2) ) by A33, A31, A32, A52, A53; :: thesis: verum
end;
hence ( 1 <= len g & g is_sequence_on G ) by ; :: thesis: verum
end;
suppose A54: n < m ; :: thesis: ex g being FinSequence of () st
( rng g c= rng f & g /. 1 in rng (Col (G,1)) & g /. (len g) in rng (Col (G,())) & 1 <= len g & g is_sequence_on G )

then A55: n in Seg m by ;
m <= m + 1 by NAT_1:11;
then reconsider l = (m + 1) - n as Element of NAT by ;
reconsider w = n - 1 as Element of NAT by ;
set f1 = f | m;
defpred S1[ Nat, set ] means \$2 = (f | m) /. (w + \$1);
A56: for i being Nat st i in Seg l holds
ex p being Point of () st S1[i,p] ;
consider g being FinSequence of () such that
A57: ( len g = l & ( for i being Nat st i in Seg l holds
S1[i,g /. i] ) ) from reconsider ww = (m + 1) - n as Element of NAT by A57;
A58: m in Seg m by ;
take g ; :: thesis: ( rng g c= rng f & g /. 1 in rng (Col (G,1)) & g /. (len g) in rng (Col (G,())) & 1 <= len g & g is_sequence_on G )
A59: dom g = Seg l by ;
A60: for i being Nat st i in Seg l holds
( n - 1 is Element of NAT & (f | m) /. (w + i) = f /. (w + i) & (n - 1) + i in dom f )
proof
let i be Nat; :: thesis: ( i in Seg l implies ( n - 1 is Element of NAT & (f | m) /. (w + i) = f /. (w + i) & (n - 1) + i in dom f ) )
assume A61: i in Seg l ; :: thesis: ( n - 1 is Element of NAT & (f | m) /. (w + i) = f /. (w + i) & (n - 1) + i in dom f )
then i <= l by FINSEQ_1:1;
then i + n <= l + n by XREAL_1:7;
then A62: (i + n) - 1 <= m by XREAL_1:20;
1 <= i by ;
then 0 + 1 <= w + i by XREAL_1:7;
then w + i in Seg m by ;
hence ( n - 1 is Element of NAT & (f | m) /. (w + i) = f /. (w + i) & (n - 1) + i in dom f ) by ; :: thesis: verum
end;
A63: now :: thesis: for i being Nat st i in dom g & i + 1 in dom g holds
for i1, i2, j1, j2 being Nat st [i1,i2] in Indices G & [j1,j2] in Indices G & g /. i = G * (i1,i2) & g /. (i + 1) = G * (j1,j2) holds
|.(i1 - j1).| + |.(i2 - j2).| = 1
let i be Nat; :: thesis: ( i in dom g & i + 1 in dom g implies for i1, i2, j1, j2 being Nat st [i1,i2] in Indices G & [j1,j2] in Indices G & g /. i = G * (i1,i2) & g /. (i + 1) = G * (j1,j2) holds
|.(i1 - j1).| + |.(i2 - j2).| = 1 )

assume that
A64: i in dom g and
A65: i + 1 in dom g ; :: thesis: for i1, i2, j1, j2 being Nat st [i1,i2] in Indices G & [j1,j2] in Indices G & g /. i = G * (i1,i2) & g /. (i + 1) = G * (j1,j2) holds
|.(i1 - j1).| + |.(i2 - j2).| = 1

g /. i = (f | m) /. (w + i) by ;
then A66: g /. i = f /. (w + i) by ;
g /. (i + 1) = (f | m) /. (w + (i + 1)) by ;
then A67: ( (w + i) + 1 in dom f & g /. (i + 1) = f /. ((w + i) + 1) ) by ;
let i1, i2, j1, j2 be Nat; :: thesis: ( [i1,i2] in Indices G & [j1,j2] in Indices G & g /. i = G * (i1,i2) & g /. (i + 1) = G * (j1,j2) implies |.(i1 - j1).| + |.(i2 - j2).| = 1 )
assume A68: ( [i1,i2] in Indices G & [j1,j2] in Indices G & g /. i = G * (i1,i2) & g /. (i + 1) = G * (j1,j2) ) ; :: thesis: |.(i1 - j1).| + |.(i2 - j2).| = 1
w + i in dom f by ;
hence |.(i1 - j1).| + |.(i2 - j2).| = 1 by A1, A66, A67, A68; :: thesis: verum
end;
A69: dom g = Seg (len g) by FINSEQ_1:def 3;
thus rng g c= rng f :: thesis: ( g /. 1 in rng (Col (G,1)) & g /. (len g) in rng (Col (G,())) & 1 <= len g & g is_sequence_on G )
proof
let z be object ; :: according to TARSKI:def 3 :: thesis: ( not z in rng g or z in rng f )
assume z in rng g ; :: thesis: z in rng f
then consider i being Element of NAT such that
A70: i in dom g and
A71: z = g /. i by PARTFUN2:2;
A72: w + i in dom f by A60, A57, A69, A70;
( z = (f | m) /. (w + i) & (f | m) /. (w + i) = f /. (w + i) ) by A60, A57, A69, A70, A71;
hence z in rng f by ; :: thesis: verum
end;
n + 1 <= m by ;
then A73: n + 1 <= m + 1 by NAT_1:13;
then A74: 1 <= l by XREAL_1:19;
then 1 in Seg l by FINSEQ_1:1;
then g /. 1 = (f | m) /. ((n - 1) + 1) by A57
.= f /. n by ;
hence g /. 1 in rng (Col (G,1)) by ; :: thesis: ( g /. (len g) in rng (Col (G,())) & 1 <= len g & g is_sequence_on G )
len g in dom g by ;
then g /. (len g) = (f | m) /. (w + ww) by
.= f /. m by ;
hence g /. (len g) in rng (Col (G,())) by ; :: thesis: ( 1 <= len g & g is_sequence_on G )
now :: thesis: for i being Nat st i in dom g holds
ex i1, i2 being Nat st
( [i1,i2] in Indices G & g /. i = G * (i1,i2) )
let i be Nat; :: thesis: ( i in dom g implies ex i1, i2 being Nat st
( [i1,i2] in Indices G & g /. i = G * (i1,i2) ) )

assume A75: i in dom g ; :: thesis: ex i1, i2 being Nat st
( [i1,i2] in Indices G & g /. i = G * (i1,i2) )

then w + i in dom f by ;
then consider i1, i2 being Nat such that
A76: ( [i1,i2] in Indices G & f /. (w + i) = G * (i1,i2) ) by A1;
take i1 = i1; :: thesis: ex i2 being Nat st
( [i1,i2] in Indices G & g /. i = G * (i1,i2) )

take i2 = i2; :: thesis: ( [i1,i2] in Indices G & g /. i = G * (i1,i2) )
g /. i = (f | m) /. (w + i) by ;
hence ( [i1,i2] in Indices G & g /. i = G * (i1,i2) ) by A60, A59, A75, A76; :: thesis: verum
end;
hence ( 1 <= len g & g is_sequence_on G ) by ; :: thesis: verum
end;
end;