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: now

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

end;

A7: now

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

per cases by A8, FINSEQ_1:38;

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

consider i, j being Element of NAT such that
A10: [i,j] in Indices G and
A11: p = G * i,j by A2;
take i = i; :: thesis:
take j = j; :: thesis:
thus [i,j] in Indices G by A10; :: thesis:
n in Seg 1 by A9, 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 <*p*> /. n = p by A9, PARTFUN1:def 8;
hence (<*p*> ^ f) /. n = G * i,j by A9, A11, 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
A12: l in dom f and
A13: n = (len <*p*>) + l ;
consider i, j being Element of NAT such that
A14: [i,j] in Indices G and
A15: f /. l = G * i,j by A1, A12, GOBOARD1:def 11;
take i = i; :: thesis:
take j = j; :: thesis:
thus [i,j] in Indices G by A14; :: thesis:
thus (<*p*> ^ f) /. n = G * i,j by A12, A13, A15, FINSEQ_4:84; :: thesis:

end;

end;

end;

A16: now

let n be Element of NAT ; :: thesis:
assume that
A17: n in dom <*p*> and
A18: n + 1 in dom <*p*> ; :: thesis:
n + 1 <= len <*p*> by A18, FINSEQ_3:27;
then A19: n + 1 <= 1 by FINSEQ_1:56;
1 <= n by A17, FINSEQ_3:27;
then 1 + 1 <= n + 1 by 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 A19, XXREAL_0:2; :: thesis:

end;

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;
then 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 A16, A4, GOBOARD1:40;
hence <*p*> ^ f is_sequence_on G by A7, GOBOARD1:def 11; :: thesis: