let G be Go-board; :: thesis:
let f be FinSequence of (TOP-REAL 2); :: thesis:
assume A1: ( f is_sequence_on G & (rng f) /\ (rng (Col G,1)) <> {} & (rng f) /\ (rng (Col G,(width G))) <> {} ) ; :: thesis:
consider x being Element of (rng f) /\ (rng (Col G,1));
A2: ( x in rng f & x in rng (Col G,1) ) by A1, XBOOLE_0:def 4;
then consider n being Element of NAT such that
A3: ( n in dom f & x = f /. n ) by PARTFUN2:4;
consider y being Element of (rng f) /\ (rng (Col G,(width G)));
A4: ( y in rng f & y in rng (Col G,(width G)) ) by A1, XBOOLE_0:def 4;
then consider m being Element of NAT such that
A5: ( m in dom f & y = f /. m ) by PARTFUN2:4;
reconsider x = x as Point of (TOP-REAL 2) by A3;
A6: ( 1 <= n & n <= len f & 1 <= m & m <= len f ) by A3, A5, FINSEQ_3:27;

per cases by XXREAL_0:1;

suppose A7: n = m ; :: thesis:

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

A9: now

let k be Element of NAT ; :: thesis:
assume A10: k in Seg 1 ; :: thesis:
then A11: k = 1 by FINSEQ_1:4, TARSKI:def 1;
k in dom h by A10, FINSEQ_1:def 8;
hence h /. k = h . k by PARTFUN1:def 8
.= x by A11, FINSEQ_1:57 ;
:: thesis:

end;

A12: rng h c= rng f

proof

let z be set ; :: according to TARSKI:def 3 :: thesis:
assume z in rng h ; :: thesis:
then consider i being Element of NAT such that
A13: ( i in dom h & z = h /. i ) by PARTFUN2:4;
i in Seg 1 by A13, FINSEQ_1:def 8;
hence z in rng f by A2, A9, A13; :: thesis:

end;

reconsider h = h as FinSequence of (TOP-REAL 2) ;
take h ; :: thesis:
thus rng h c= rng f by A12; :: thesis:
A14: 1 in Seg 1 by FINSEQ_1:3;
then A15: ( h /. 1 = x & h /. (len h) = x & dom h = Seg (len h) ) by A8, A9, FINSEQ_1:def 3;
thus ( h /. 1 in rng (Col G,1) & h /. (len h) in rng (Col G,(width G)) ) by A2, A3, A4, A5, A7, A8, A9, A14; :: thesis:

A16: now

let i be Element of NAT ; :: thesis:
assume A17: i in dom h ; :: thesis:
consider i1, i2 being Element of NAT such that
A18: ( [i1,i2] in Indices G & f /. n = G * i1,i2 ) by A1, A3, Def11;
take i1 = i1; :: thesis:
take i2 = i2; :: thesis:
thus ( [i1,i2] in Indices G & h /. i = G * i1,i2 ) by A3, A8, A9, A15, A17, A18; :: thesis:

end;

now

let i be Element of NAT ; :: thesis:
assume ( i in dom h & i + 1 in dom h ) ; :: thesis:
then ( i = 1 & i + 1 = 1 ) by A8, A15, FINSEQ_1:4, TARSKI:def 1;
hence for i1, i2, j1, j2 being Element of NAT st [i1,i2] in Indices G & [j1,j2] in Indices G & h /. i = G * i1,i2 & h /. (i + 1) = G * j1,j2 holds
(abs (i1 - j1)) + (abs (i2 - j2)) = 1 ; :: thesis:

end;

hence ( 1 <= len h & h is_sequence_on G ) by A16, Def11, FINSEQ_1:56; :: thesis:

end;

suppose A19: n > m ; :: thesis:

set f1 = f | n;
( m <= n & n <= n + 1 ) by A19, NAT_1:11;
then reconsider l = (n + 1) - m as Element of NAT by INT_1:18, XXREAL_0:2;

A20: now

let i be Element of NAT ; :: thesis:
assume i in Seg l ; :: thesis:
then A21: ( 1 <= i & i <= l & 0 <= m ) by FINSEQ_1:3;
l <= (n + 1) - 0 by XREAL_1:15;
hence (n + 1) - i is Element of NAT by A21, INT_1:18, XXREAL_0:2; :: thesis:

end;

A22: for i being Element of 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 Element of NAT ; :: thesis:
assume i in Seg l ; :: thesis:
then A23: ( 1 <= i & i <= l & 0 <= m ) by FINSEQ_1:3;
l <= (n + 1) - 0 by XREAL_1:15;
then reconsider w = (n + 1) - i as Element of NAT by A23, INT_1:18, XXREAL_0:2;
A24: ( (n + 1) - i <= (n + 1) - 1 & (n + 1) - l <= (n + 1) - i ) by A23, XREAL_1:15;
then 1 <= (n + 1) - i by A6, XXREAL_0:2;
then w in Seg n by A24, FINSEQ_1:3;
hence ( (n + 1) - i is Element of NAT & (f | n) /. ((n + 1) - i) = f /. ((n + 1) - i) & (n + 1) - i in dom f ) by A3, FINSEQ_4:86; :: thesis:

end;

defpred S₁[ Nat, set ] means for k being Element of NAT st $1 + k = n + 1 holds
$2 = (f | n) /. k;
A25: 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 A20;
take (f | n) /. a ; :: thesis:
let k be Element of 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
A26: ( len g = l & ( for i being Nat st i in Seg l holds
S₁[i,g /. i] ) ) from FINSEQ_4:sch 1(A25);
A27: dom g = Seg (len g) by FINSEQ_1:def 3;
take g ; :: thesis:
thus rng g c= rng f :: thesis:

proof

let z be set ; :: according to TARSKI:def 3 :: thesis:
assume z in rng g ; :: thesis:
then consider i being Element of NAT such that
A28: ( i in dom g & z = g /. i ) by PARTFUN2:4;
reconsider yy = (n + 1) - i as Element of NAT by A20, A26, A27, A28;
i + yy = n + 1 ;
then ( z = (f | n) /. yy & (f | n) /. yy = f /. yy & yy in dom f ) by A22, A26, A27, A28;
hence z in rng f by PARTFUN2:4; :: thesis:

end;

( m + 1 <= n & n <= n + 1 ) by A19, NAT_1:13;
then A29: ( m + 1 <= n + 1 & dom g = Seg (len g) ) by FINSEQ_1:def 3, XXREAL_0:2;
then ( m <= n & 1 <= l & len g = l ) by A26, XREAL_1:8, XREAL_1:21;
then A30: ( 1 in Seg l & m in Seg n & len g in dom g & n in Seg n ) by A6, FINSEQ_1:3, FINSEQ_3:27;
then g /. 1 = (f | n) /. n by A26
.= f /. n by A3, A30, FINSEQ_4:86 ;
hence g /. 1 in rng (Col G,1) by A1, A3, XBOOLE_0:def 4; :: thesis:
reconsider ww = (n + 1) - l as Element of NAT ;
l + ww = n + 1 ;
then g /. (len g) = (f | n) /. ww by A26, A27, A30
.= f /. m by A3, A30, FINSEQ_4:86 ;
hence g /. (len g) in rng (Col G,(width G)) by A1, A5, XBOOLE_0:def 4; :: thesis:

A31: now

let i be Element of NAT ; :: thesis:
assume A32: i in dom g ; :: thesis:
then reconsider ww = (n + 1) - i as Element of NAT by A20, A26, A29;
i + ww = n + 1 ;
then A33: ( i in Seg l & dom g = Seg l & g /. i = (f | n) /. ww ) by A26, A27, A32;
then ( ww in dom f & g /. i = f /. ww ) by A22;
then consider i1, i2 being Element of NAT such that
A34: ( [i1,i2] in Indices G & f /. ww = G * i1,i2 ) by A1, Def11;
take i1 = i1; :: thesis:
take i2 = i2; :: thesis:
thus ( [i1,i2] in Indices G & g /. i = G * i1,i2 ) by A22, A33, A34; :: thesis:

end;

now

let i be Element of NAT ; :: thesis:
assume A35: ( i in dom g & i + 1 in dom g ) ; :: thesis:
then reconsider ww = (n + 1) - i as Element of NAT by A20, A26, A29;
reconsider xx = (n + 1) - (i + 1) as Element of NAT by A20, A26, A29, A35;
( i + ww = n + 1 & (i + 1) + xx = n + 1 ) ;
then ( i in Seg l & i + 1 in Seg l & dom g = Seg l & g /. i = (f | n) /. ww & g /. (i + 1) = (f | n) /. xx & (n + 1) - (i + 1) = ((n + 1) - i) - 1 ) by A26, A27, A35;
then A36: ( ww in dom f & g /. i = f /. ww & xx in dom f & g /. (i + 1) = f /. xx ) by A22;
A37: xx + 1 = (n + 1) - i ;
let i1, i2, j1, j2 be Element of NAT ; :: thesis:
assume ( [i1,i2] in Indices G & [j1,j2] in Indices G & g /. i = G * i1,i2 & g /. (i + 1) = G * j1,j2 ) ; :: thesis:
hence 1 = (abs (j1 - i1)) + (abs (j2 - i2)) by A1, A36, A37, Def11
.= (abs (- (i1 - j1))) + (abs (- (i2 - j2)))
.= (abs (i1 - j1)) + (abs (- (i2 - j2))) by COMPLEX1:138
.= (abs (i1 - j1)) + (abs (i2 - j2)) by COMPLEX1:138 ;
:: thesis:

end;

hence ( 1 <= len g & g is_sequence_on G ) by A26, A29, A31, Def11, XREAL_1:21; :: thesis:

end;

suppose A38: n < m ; :: thesis:

set f1 = f | m;
( n <= m & m <= m + 1 ) by A38, NAT_1:11;
then reconsider l = (m + 1) - n as Element of NAT by INT_1:18, XXREAL_0:2;
reconsider w = n - 1 as Element of NAT by A6, INT_1:18;
A39: for i being Element of 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 Element of NAT ; :: thesis:
assume i in Seg l ; :: thesis:
then ( 0 <= w & 1 <= i & i <= l ) by FINSEQ_1:3;
then A40: ( 0 + 1 <= w + i & i + n <= l + n ) by XREAL_1:9;
then (i + n) - 1 <= m by XREAL_1:22;
then w + i in Seg m by A40, FINSEQ_1:3;
hence ( n - 1 is Element of NAT & (f | m) /. (w + i) = f /. (w + i) & (n - 1) + i in dom f ) by A5, FINSEQ_4:86; :: thesis:

end;

defpred S₁[ Nat, set ] means $2 = (f | m) /. (w + $1);
A41: 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
A42: ( len g = l & ( for i being Nat st i in Seg l holds
S₁[i,g /. i] ) ) from FINSEQ_4:sch 1(A41);
A43: dom g = Seg l by A42, FINSEQ_1:def 3;
take g ; :: thesis:
A44: dom g = Seg (len g) by FINSEQ_1:def 3;
thus rng g c= rng f :: thesis:

proof

let z be set ; :: according to TARSKI:def 3 :: thesis:
assume z in rng g ; :: thesis:
then consider i being Element of NAT such that
A45: ( i in dom g & z = g /. i ) by PARTFUN2:4;
( z = (f | m) /. (w + i) & (f | m) /. (w + i) = f /. (w + i) & w + i in dom f ) by A39, A42, A44, A45;
hence z in rng f by PARTFUN2:4; :: thesis:

end;

( n + 1 <= m & m <= m + 1 ) by A38, NAT_1:13;
then A46: ( n + 1 <= m + 1 & dom g = Seg (len g) ) by FINSEQ_1:def 3, XXREAL_0:2;
then ( n <= m & 1 <= l & len g = l ) by A42, XREAL_1:8, XREAL_1:21;
then A47: ( 1 in Seg l & n in Seg m & len g in dom g & m in Seg m ) by A6, FINSEQ_1:3, FINSEQ_3:27;
then g /. 1 = (f | m) /. ((n - 1) + 1) by A42
.= f /. n by A5, A47, FINSEQ_4:86 ;
hence g /. 1 in rng (Col G,1) by A1, A3, XBOOLE_0:def 4; :: thesis:
reconsider ww = (m + 1) - n as Element of NAT by A42;
g /. (len g) = (f | m) /. (w + ww) by A42, A43, A47
.= f /. m by A5, A47, FINSEQ_4:86 ;
hence g /. (len g) in rng (Col G,(width G)) by A1, A5, XBOOLE_0:def 4; :: thesis:

A48: now

let i be Element of NAT ; :: thesis:
assume i in dom g ; :: thesis:
then A49: ( i in Seg l & dom g = Seg l & g /. i = (f | m) /. (w + i) ) by A42, A43;
then ( w + i in dom f & g /. i = f /. (w + i) ) by A39;
then consider i1, i2 being Element of NAT such that
A50: ( [i1,i2] in Indices G & f /. (w + i) = G * i1,i2 ) by A1, Def11;
take i1 = i1; :: thesis:
take i2 = i2; :: thesis:
thus ( [i1,i2] in Indices G & g /. i = G * i1,i2 ) by A39, A49, A50; :: thesis:

end;

now

let i be Element of NAT ; :: thesis:
assume ( i in dom g & i + 1 in dom g ) ; :: thesis:
then ( i in Seg l & i + 1 in Seg l & dom g = Seg l & g /. i = (f | m) /. (w + i) & g /. (i + 1) = (f | m) /. (w + (i + 1)) & w + (i + 1) = (w + i) + 1 ) by A42, A43;
then A51: ( w + i in dom f & g /. i = f /. (w + i) & (w + i) + 1 in dom f & g /. (i + 1) = f /. ((w + i) + 1) ) by A39;
let i1, i2, j1, j2 be Element of NAT ; :: thesis:
assume ( [i1,i2] in Indices G & [j1,j2] in Indices G & g /. i = G * i1,i2 & g /. (i + 1) = G * j1,j2 ) ; :: thesis:
hence (abs (i1 - j1)) + (abs (i2 - j2)) = 1 by A1, A51, Def11; :: thesis:

end;

hence ( 1 <= len g & g is_sequence_on G ) by A42, A46, A48, Def11, XREAL_1:21; :: thesis:

end;