let G be Go-board; :: thesis:
let p be Point of (TOP-REAL 2); :: thesis:
let f be 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 & p = G * i1,j1 & f /. 1 = 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 & <*p*> /. (len <*p*>) = G * m,k & f /. 1 = G * i,j ) and
A7: ( len <*p*> in dom <*p*> & 1 in dom f ) ; :: thesis:
len <*p*> = 1 by FINSEQ_1:57;
then <*p*> . (len <*p*>) = p by FINSEQ_1:57;
then <*p*> /. (len <*p*>) = p by A7, PARTFUN1:def 8;
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 A8: for n being Element of NAT st n in dom (<*p*> ^ f) & n + 1 in dom (<*p*> ^ f) holds
for m, k, i, j being Element of NAT st [m,k] in Indices G & [i,j] in Indices G & (<*p*> ^ f) /. n = G * m,k & (<*p*> ^ f) /. (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 A9: n in dom (<*p*> ^ f) ; :: thesis:

per cases by A9, FINSEQ_1:38;

suppose A10: n in dom <*p*> ; :: thesis:

then n in Seg 1 by FINSEQ_1:55;
then ( 1 <= n & n <= 1 ) by FINSEQ_1:3;
then n = 1 by XXREAL_0:1;
then <*p*> . n = p by FINSEQ_1:57;
then A11: <*p*> /. n = p by A10, PARTFUN1:def 8;
consider i, j being Element of NAT such that
A12: [i,j] in Indices G and
A13: p = G * i,j by A2;
take i = i; :: thesis:
take j = j; :: thesis:
thus [i,j] in Indices G by A12; :: thesis:
thus (<*p*> ^ f) /. n = G * i,j by A10, A11, A13, FINSEQ_4:83; :: thesis:

end;

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

then consider l being Nat such that
A14: l in dom f and
A15: n = (len <*p*>) + l ;
consider i, j being Element of NAT such that
A16: [i,j] in Indices G and
A17: f /. l = G * i,j by A1, A14, GOBOARD1:def 11;
take i = i; :: thesis:
take j = j; :: thesis:
thus [i,j] in Indices G by A16; :: thesis:
thus (<*p*> ^ f) /. n = G * i,j by A14, A15, A17, FINSEQ_4:84; :: thesis:

end;

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