let G be Go-board; :: thesis:
let p be Point of (TOP-REAL 2); :: thesis:
let f be non empty FinSequence of (TOP-REAL 2); :: thesis:
assume that
A1: f is_sequence_on G and
A2: ex i, j being Element of NAT st
( [i,j] in Indices G & p = G * i,j ) and
A3: for i1, j1, i2, j2 being Element of NAT st [i1,j1] in Indices G & [i2,j2] in Indices G & f /. (len f) = G * i1,j1 & p = G * i2,j2 holds
(abs (i2 - i1)) + (abs (j2 - j1)) = 1 ; :: thesis:
A4: for n being Element of NAT st n in dom f & n + 1 in dom f holds
for m, k, i, j being Element of NAT st [m,k] in Indices G & [i,j] in Indices G & f /. n = G * m,k & f /. (n + 1) = G * i,j holds
(abs (m - i)) + (abs (k - j)) = 1 by A1, GOBOARD1:def 11;

A5: now

let n be Element of NAT ; :: thesis:
assume ( n in dom <*p*> & n + 1 in dom <*p*> ) ; :: thesis:
then ( 1 <= n & n + 1 <= len <*p*> ) by FINSEQ_3:27;
then ( 1 + 1 <= n + 1 & n + 1 <= 1 ) by FINSEQ_1:56, XREAL_1:8;
hence for m, k, i, j being Element of NAT st [m,k] in Indices G & [i,j] in Indices G & <*p*> /. n = G * m,k & <*p*> /. (n + 1) = G * i,j holds
(abs (m - i)) + (abs (k - j)) = 1 by XXREAL_0:2; :: thesis:

end;

now

let m, k, i, j be Element of NAT ; :: thesis:
assume that
A6: ( [m,k] in Indices G & [i,j] in Indices G & f /. (len f) = G * m,k & <*p*> /. 1 = G * i,j ) and
( len f in dom f & 1 in dom <*p*> ) ; :: thesis:
<*p*> /. 1 = p by FINSEQ_4:25;
then (abs (i - m)) + (abs (j - k)) = 1 by A3, A6;
hence 1 = (abs (m - i)) + (abs (j - k)) by UNIFORM1:13
.= (abs (m - i)) + (abs (k - j)) by UNIFORM1:13 ;
:: thesis:

end;

then A7: for n being Element of NAT st n in dom (f ^ <*p*>) & n + 1 in dom (f ^ <*p*>) holds
for m, k, i, j being Element of NAT st [m,k] in Indices G & [i,j] in Indices G & (f ^ <*p*>) /. n = G * m,k & (f ^ <*p*>) /. (n + 1) = G * i,j holds
(abs (m - i)) + (abs (k - j)) = 1 by A4, A5, GOBOARD1:40;

let n be Element of NAT ; :: thesis:
assume A8: n in dom (f ^ <*p*>) ; :: thesis:

per cases by A8, FINSEQ_1:38;

suppose A9: n in dom f ; :: thesis:

then consider i, j being Element of NAT such that
A10: [i,j] in Indices G and
A11: f /. n = G * i,j by A1, GOBOARD1:def 11;
take i = i; :: thesis:
take j = j; :: thesis:
thus [i,j] in Indices G by A10; :: thesis:
thus (f ^ <*p*>) /. n = G * i,j by A9, A11, FINSEQ_4:83; :: thesis:

end;

suppose ex l being Nat st
( l in dom <*p*> & n = (len f) + l ) ; :: thesis:

then consider l being Nat such that
A12: l in dom <*p*> and
A13: n = (len f) + l ;
consider i, j being Element of NAT such that
A14: [i,j] in Indices G and
A15: p = G * i,j by A2;
take i = i; :: thesis:
take j = j; :: thesis:
thus [i,j] in Indices G by A14; :: thesis:
( 1 <= l & l <= len <*p*> ) by A12, FINSEQ_3:27;
then ( 1 <= l & l <= 1 ) by FINSEQ_1:56;
then l = 1 by XXREAL_0:1;
then <*p*> /. l = p by FINSEQ_4:25;
hence (f ^ <*p*>) /. n = G * i,j by A12, A13, A15, FINSEQ_4:84; :: thesis:

end;

hence f ^ <*p*> is_sequence_on G by A7, GOBOARD1:def 11; :: thesis: