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 Nat st
( [i,j] in Indices G & p = G * (i,j) ) and
A3: for i1, j1, i2, j2 being Nat st [i1,j1] in Indices G & [i2,j2] in Indices G & p = G * (i1,j1) & f /. 1 = G * (i2,j2) holds
|.(i2 - i1).| + |.(j2 - j1).| = 1 ; :: thesis:

A4: now :: thesis:

let m, k, i, j be 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:40;
then <*p*> . (len <*p*>) = p by FINSEQ_1:40;
then <*p*> /. (len <*p*>) = p by A6, PARTFUN1:def 6;
then |.(i - m).| + |.(j - k).| = 1 by A3, A5;
hence 1 = |.(m - i).| + |.(j - k).| by UNIFORM1:11
.= |.(m - i).| + |.(k - j).| by UNIFORM1:11 ;
:: thesis:

end;

A7: now :: thesis:

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

per cases by A8, FINSEQ_1:25;

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

consider i, j being 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:38;
then ( 1 <= n & n <= 1 ) by FINSEQ_1:1;
then n = 1 by XXREAL_0:1;
then <*p*> . n = p by FINSEQ_1:40;
then <*p*> /. n = p by A9, PARTFUN1:def 6;
hence (<*p*> ^ f) /. n = G * (i,j) by A9, A11, FINSEQ_4:68; :: 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 Nat such that
A14: [i,j] in Indices G and
A15: f /. l = G * (i,j) by A1, A12, GOBOARD1:def 9;
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:69; :: thesis:

end;

end;

end;

A16: now :: thesis:

let n be 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:25;
then A19: n + 1 <= 1 by FINSEQ_1:39;
1 <= n by A17, FINSEQ_3:25;
then 1 + 1 <= n + 1 by XREAL_1:6;
hence for m, k, i, j being Nat st [m,k] in Indices G & [i,j] in Indices G & <*p*> /. n = G * (m,k) & <*p*> /. (n + 1) = G * (i,j) holds
|.(m - i).| + |.(k - j).| = 1 by A19, XXREAL_0:2; :: thesis:

end;

for n being Nat st n in dom f & n + 1 in dom f holds
for m, k, i, j being Nat st [m,k] in Indices G & [i,j] in Indices G & f /. n = G * (m,k) & f /. (n + 1) = G * (i,j) holds
|.(m - i).| + |.(k - j).| = 1 by A1, GOBOARD1:def 9;
then for n being Nat st n in dom (<*p*> ^ f) & n + 1 in dom (<*p*> ^ f) holds
for m, k, i, j being 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
|.(m - i).| + |.(k - j).| = 1 by A16, A4, GOBOARD1:24;
hence <*p*> ^ f is_sequence_on G by A7, GOBOARD1:def 9; :: thesis: