let G be Go-board; :: thesis:
let f be FinSequence of (TOP-REAL 2); :: thesis:
assume that
A1: f is_sequence_on G and
A2: (rng f) /\ (rng (Col (G,1))) <> {} and
A3: (rng f) /\ (rng (Col (G,(width G)))) <> {} ; :: thesis:
set y = the Element of (rng f) /\ (rng (Col (G,(width 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,(width G)))) in rng (Col (G,(width G))) ) by A2, A3, XBOOLE_0:def 4;
the Element of (rng f) /\ (rng (Col (G,(width G)))) in rng f by A3, XBOOLE_0:def 4;
then consider m being Element of NAT such that
A5: m in dom f and
A6: the Element of (rng f) /\ (rng (Col (G,(width G)))) = f /. m by PARTFUN2:2;
A7: 1 <= m by A5, FINSEQ_3:25;
A8: the Element of (rng f) /\ (rng (Col (G,1))) in rng f by A2, XBOOLE_0:def 4;
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 (TOP-REAL 2) by A10;
A11: 1 <= n by A9, FINSEQ_3:25;

reconsider h = <*x*> as FinSequence of (TOP-REAL 2) ;
A13: len h = 1 by FINSEQ_1:39;

A14: now :: thesis:

let k be Nat; :: thesis:
assume A15: k in Seg 1 ; :: thesis:
then A16: k = 1 by FINSEQ_1:2, TARSKI:def 1;
k in dom h by A15, FINSEQ_1:def 8;
hence h /. k = h . k by PARTFUN1:def 6
.= x by A16 ;
:: thesis:

end;

A17: rng h c= rng f

proof

let z be object ; :: according to TARSKI:def 3 :: thesis:
assume z in rng h ; :: thesis:
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 A18, FINSEQ_1:def 8;
hence z in rng f by A8, A14, A19; :: thesis:

end;

reconsider h = h as FinSequence of (TOP-REAL 2) ;
take h ; :: thesis:
thus rng h c= rng f by A17; :: thesis:
1 in Seg 1 by FINSEQ_1:1;
hence ( h /. 1 in rng (Col (G,1)) & h /. (len h) in rng (Col (G,(width G))) ) by A10, A4, A6, A12, A13, A14; :: thesis:
A20: dom h = Seg (len h) by FINSEQ_1:def 3;

A21: now :: thesis:

let i be Nat; :: thesis:
assume that
A22: i in dom h and
A23: i + 1 in dom h ; :: thesis:
i = 1 by A13, A20, A22, FINSEQ_1:2, TARSKI:def 1;
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 A13, A20, A23, FINSEQ_1:2, TARSKI:def 1; :: thesis:

end;

now :: thesis:

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:
assume A25: i in dom h ; :: thesis:
take i1 = i1; :: thesis:
take i2 = i2; :: thesis:
thus ( [i1,i2] in Indices G & h /. i = G * (i1,i2) ) by A10, A13, A14, A20, A25, A24; :: thesis:

end;

hence ( 1 <= len h & h is_sequence_on G ) by A21, FINSEQ_1:39; :: thesis:

end;

suppose A26: n > m ; :: thesis:

n <= n + 1 by NAT_1:11;
then reconsider l = (n + 1) - m as Element of NAT by A26, INT_1:5, XXREAL_0:2;
set f1 = f | n;
defpred S₁[ Nat, set ] means for k being Nat st $1 + k = n + 1 holds
$2 = (f | n) /. k;
A27: n in Seg n by A11, FINSEQ_1:1;

A28: now :: thesis:

let i be Nat; :: thesis:
assume i in Seg l ; :: thesis:
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 A29, INT_1:5, XXREAL_0:2; :: thesis:

end;

A30: for i being Nat st i in Seg l holds
ex p being Point of (TOP-REAL 2) st S₁[i,p]

proof

let i be Nat; :: thesis:
assume i in Seg l ; :: thesis:
then reconsider a = (n + 1) - i as Element of NAT by A28;
take (f | n) /. a ; :: thesis:
let k be Nat; :: thesis:
assume i + k = n + 1 ; :: thesis:
hence (f | n) /. a = (f | n) /. k ; :: thesis:

end;

consider g being FinSequence of (TOP-REAL 2) such that
A31: ( len g = l & ( for i being Nat st i in Seg l holds
S₁[i,g /. i] ) ) from FINSEQ_4:sch 1(A30);
take g ; :: thesis:
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:
assume A34: i in Seg l ; :: thesis:
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 A35, INT_1:5, XXREAL_0:2;
1 <= i by A34, FINSEQ_1:1;
then A36: (n + 1) - i <= (n + 1) - 1 by XREAL_1:13;
(n + 1) - l <= (n + 1) - i by A35, XREAL_1:13;
then 1 <= (n + 1) - i by A7, XXREAL_0:2;
then w in Seg n by A36, FINSEQ_1:1;
hence ( (n + 1) - i is Element of NAT & (f | n) /. ((n + 1) - i) = f /. ((n + 1) - i) & (n + 1) - i in dom f ) by A9, FINSEQ_4:71; :: thesis:

end;

thus rng g c= rng f :: thesis:

proof

let z be object ; :: according to TARSKI:def 3 :: thesis:
assume z in rng g ; :: thesis:
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 A39, PARTFUN2:2; :: thesis:

end;

A40: dom g = Seg (len g) by FINSEQ_1:def 3;

A41: now :: thesis:

let i be Nat; :: thesis:
assume that
A42: i in dom g and
A43: i + 1 in dom g ; :: thesis:
let i1, i2, j1, j2 be Nat; :: thesis:
assume A44: ( [i1,i2] in Indices G & [j1,j2] in Indices G & g /. i = G * (i1,i2) & g /. (i + 1) = G * (j1,j2) ) ; :: thesis:
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 A31, A32, A43;
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 A31, A32, A42;
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:

end;

m + 1 <= n by A26, NAT_1:13;
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 A9, A27, FINSEQ_4:71 ;
hence g /. 1 in rng (Col (G,1)) by A2, A10, XBOOLE_0:def 4; :: thesis:
A50: m in Seg n by A7, A26, FINSEQ_1:1;
reconsider ww = (n + 1) - l as Element of NAT ;
A51: l + ww = n + 1 ;
len g in dom g by A31, A49, FINSEQ_3:25;
then g /. (len g) = (f | n) /. ww by A31, A32, A51
.= f /. m by A9, A50, FINSEQ_4:71 ;
hence g /. (len g) in rng (Col (G,(width G))) by A3, A6, XBOOLE_0:def 4; :: thesis:

now :: thesis:

let i be Nat; :: thesis:
assume A52: i in dom g ; :: thesis:
then reconsider ww = (n + 1) - i as Element of NAT by A28, A31, A40;
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:
take i2 = i2; :: thesis:
i + ww = n + 1 ;
then g /. i = (f | n) /. ww by A31, A32, A52;
hence ( [i1,i2] in Indices G & g /. i = G * (i1,i2) ) by A33, A31, A32, A52, A53; :: thesis:

end;

hence ( 1 <= len g & g is_sequence_on G ) by A31, A48, A41, XREAL_1:19; :: thesis:

end;

suppose A54: n < m ; :: thesis:

then A55: n in Seg m by A11, FINSEQ_1:1;
m <= m + 1 by NAT_1:11;
then reconsider l = (m + 1) - n as Element of NAT by A54, INT_1:5, XXREAL_0:2;
reconsider w = n - 1 as Element of NAT by A11, INT_1:5;
set f1 = f | m;
defpred S₁[ Nat, set ] means $2 = (f | m) /. (w + $1);
A56: for i being Nat st i in Seg l holds
ex p being Point of (TOP-REAL 2) st S₁[i,p] ;
consider g being FinSequence of (TOP-REAL 2) such that
A57: ( len g = l & ( for i being Nat st i in Seg l holds
S₁[i,g /. i] ) ) from FINSEQ_4:sch 1(A56);
reconsider ww = (m + 1) - n as Element of NAT by A57;
A58: m in Seg m by A7, FINSEQ_1:1;
take g ; :: thesis:
A59: dom g = Seg l by A57, FINSEQ_1:def 3;
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:
assume A61: i in Seg l ; :: thesis:
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 A61, FINSEQ_1:1;
then 0 + 1 <= w + i by XREAL_1:7;
then w + i in Seg m by A62, FINSEQ_1:1;
hence ( n - 1 is Element of NAT & (f | m) /. (w + i) = f /. (w + i) & (n - 1) + i in dom f ) by A5, FINSEQ_4:71; :: thesis:

end;

A63: now :: thesis:

let i be Nat; :: thesis:
assume that
A64: i in dom g and
A65: i + 1 in dom g ; :: thesis:
g /. i = (f | m) /. (w + i) by A57, A59, A64;
then A66: g /. i = f /. (w + i) by A60, A59, A64;
g /. (i + 1) = (f | m) /. (w + (i + 1)) by A57, A59, A65;
then A67: ( (w + i) + 1 in dom f & g /. (i + 1) = f /. ((w + i) + 1) ) by A60, A59, A65;
let i1, i2, j1, j2 be Nat; :: thesis:
assume A68: ( [i1,i2] in Indices G & [j1,j2] in Indices G & g /. i = G * (i1,i2) & g /. (i + 1) = G * (j1,j2) ) ; :: thesis:
w + i in dom f by A60, A59, A64;
hence |.(i1 - j1).| + |.(i2 - j2).| = 1 by A1, A66, A67, A68; :: thesis:

end;

A69: dom g = Seg (len g) by FINSEQ_1:def 3;
thus rng g c= rng f :: thesis:

proof

let z be object ; :: according to TARSKI:def 3 :: thesis:
assume z in rng g ; :: thesis:
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 A72, PARTFUN2:2; :: thesis:

end;

n + 1 <= m by A54, NAT_1:13;
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 A5, A55, FINSEQ_4:71 ;
hence g /. 1 in rng (Col (G,1)) by A2, A10, XBOOLE_0:def 4; :: thesis:
len g in dom g by A57, A74, FINSEQ_3:25;
then g /. (len g) = (f | m) /. (w + ww) by A57, A59
.= f /. m by A5, A58, FINSEQ_4:71 ;
hence g /. (len g) in rng (Col (G,(width G))) by A3, A6, XBOOLE_0:def 4; :: thesis:

now :: thesis:

let i be Nat; :: thesis:
assume A75: i in dom g ; :: thesis:
then w + i in dom f by A60, A59;
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:
take i2 = i2; :: thesis:
g /. i = (f | m) /. (w + i) by A57, A59, A75;
hence ( [i1,i2] in Indices G & g /. i = G * (i1,i2) ) by A60, A59, A75, A76; :: thesis:

end;

hence ( 1 <= len g & g is_sequence_on G ) by A57, A73, A63, XREAL_1:19; :: thesis:

end;