let G be Go-board; :: thesis: for p being Point of (TOP-REAL 2)
for f being non empty FinSequence of (TOP-REAL 2) st f is_sequence_on G & ex i, j being Nat st
( [i,j] in Indices G & p = G * (i,j) ) & ( for i1, j1, i2, j2 being Nat st [i1,j1] in Indices G & [i2,j2] in Indices G & f /. (len f) = G * (i1,j1) & p = G * (i2,j2) holds
|.(i2 - i1).| + |.(j2 - j1).| = 1 ) holds
f ^ <*p*> is_sequence_on G
let p be Point of (TOP-REAL 2); :: thesis: for f being non empty FinSequence of (TOP-REAL 2) st f is_sequence_on G & ex i, j being Nat st
( [i,j] in Indices G & p = G * (i,j) ) & ( for i1, j1, i2, j2 being Nat st [i1,j1] in Indices G & [i2,j2] in Indices G & f /. (len f) = G * (i1,j1) & p = G * (i2,j2) holds
|.(i2 - i1).| + |.(j2 - j1).| = 1 ) holds
f ^ <*p*> is_sequence_on G
let f be non empty FinSequence of (TOP-REAL 2); :: thesis: ( f is_sequence_on G & ex i, j being Nat st
( [i,j] in Indices G & p = G * (i,j) ) & ( for i1, j1, i2, j2 being Nat st [i1,j1] in Indices G & [i2,j2] in Indices G & f /. (len f) = G * (i1,j1) & p = G * (i2,j2) holds
|.(i2 - i1).| + |.(j2 - j1).| = 1 ) implies f ^ <*p*> is_sequence_on G )
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 & f /. (len f) = G * (i1,j1) & p = G * (i2,j2) holds
|.(i2 - i1).| + |.(j2 - j1).| = 1 ; :: thesis: f ^ <*p*> is_sequence_on G
A4: 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;

A5: now :: thesis: for n being Nat st n in dom <*p*> & n + 1 in dom <*p*> holds
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

let n be Nat; :: thesis: ( n in dom <*p*> & n + 1 in dom <*p*> implies 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 )
assume that
A6: n in dom <*p*> and
A7: n + 1 in dom <*p*> ; :: thesis: 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
A8: 1 <= n by A6, FINSEQ_3:25;
A9: n + 1 <= len <*p*> by A7, FINSEQ_3:25;
A10: 1 + 1 <= n + 1 by A8, XREAL_1:6;
n + 1 <= 1 by A9, FINSEQ_1:39;
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 A10, XXREAL_0:2; :: thesis: verum

end;

now :: thesis: for m, k, i, j being Nat st [m,k] in Indices G & [i,j] in Indices G & f /. (len f) = G * (m,k) & <*p*> /. 1 = G * (i,j) & len f in dom f & 1 in dom <*p*> holds
1 = |.(m - i).| + |.(k - j).|

let m, k, i, j be Nat; :: thesis: ( [m,k] in Indices G & [i,j] in Indices G & f /. (len f) = G * (m,k) & <*p*> /. 1 = G * (i,j) & len f in dom f & 1 in dom <*p*> implies 1 = |.(m - i).| + |.(k - j).| )
assume that
A11: [m,k] in Indices G and
A12: [i,j] in Indices G and
A13: f /. (len f) = G * (m,k) and
A14: <*p*> /. 1 = G * (i,j) and
len f in dom f and
1 in dom <*p*> ; :: thesis: 1 = |.(m - i).| + |.(k - j).|
<*p*> /. 1 = p by FINSEQ_4:16;
then |.(i - m).| + |.(j - k).| = 1 by A3, A11, A12, A13, A14;
hence 1 = |.(m - i).| + |.(j - k).| by UNIFORM1:11
.= |.(m - i).| + |.(k - j).| by UNIFORM1:11 ;
:: thesis: verum

end;

then A15: for n being Nat st n in dom (f ^ <*p*>) & n + 1 in dom (f ^ <*p*>) holds
for m, k, i, j being 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
|.(m - i).| + |.(k - j).| = 1 by A4, A5, GOBOARD1:24;

now :: thesis: for n being Nat st n in dom (f ^ <*p*>) holds
ex i, j being Nat st
( [i,j] in Indices G & (f ^ <*p*>) /. n = G * (i,j) )

let n be Nat; :: thesis: ( n in dom (f ^ <*p*>) implies ex i, j being Nat st
( [j,b₃] in Indices G & (f ^ <*p*>) /. i = G * (j,b₃) ) )
assume A16: n in dom (f ^ <*p*>) ; :: thesis: ex i, j being Nat st
( [j,b₃] in Indices G & (f ^ <*p*>) /. i = G * (j,b₃) )

per cases ( n in dom f or ex l being Nat st
( l in dom <*p*> & n = (len f) + l ) ) by A16, FINSEQ_1:25;

suppose A17: n in dom f ; :: thesis: ex i, j being Nat st
( [j,b₃] in Indices G & (f ^ <*p*>) /. i = G * (j,b₃) )

then consider i, j being Nat such that
A18: [i,j] in Indices G and
A19: f /. n = G * (i,j) by A1;
take i = i; :: thesis: ex j being Nat st
( [i,j] in Indices G & (f ^ <*p*>) /. n = G * (i,j) )
take j = j; :: thesis: ( [i,j] in Indices G & (f ^ <*p*>) /. n = G * (i,j) )
thus [i,j] in Indices G by A18; :: thesis: (f ^ <*p*>) /. n = G * (i,j)
thus (f ^ <*p*>) /. n = G * (i,j) by A17, A19, FINSEQ_4:68; :: thesis: verum

end;

suppose ex l being Nat st
( l in dom <*p*> & n = (len f) + l ) ; :: thesis: ex i, j being Nat st
( [j,b₃] in Indices G & (f ^ <*p*>) /. i = G * (j,b₃) )

then consider l being Nat such that
A20: l in dom <*p*> and
A21: n = (len f) + l ;
consider i, j being Nat such that
A22: [i,j] in Indices G and
A23: p = G * (i,j) by A2;
take i = i; :: thesis: ex j being Nat st
( [i,j] in Indices G & (f ^ <*p*>) /. n = G * (i,j) )
take j = j; :: thesis: ( [i,j] in Indices G & (f ^ <*p*>) /. n = G * (i,j) )
thus [i,j] in Indices G by A22; :: thesis: (f ^ <*p*>) /. n = G * (i,j)
A24: l <= len <*p*> by A20, FINSEQ_3:25;
A25: 1 <= l by A20, FINSEQ_3:25;
l <= 1 by A24, FINSEQ_1:39;
then l = 1 by A25, XXREAL_0:1;
then <*p*> /. l = p by FINSEQ_4:16;
hence (f ^ <*p*>) /. n = G * (i,j) by A20, A21, A23, FINSEQ_4:69; :: thesis: verum

end;

end;

end;

hence f ^ <*p*> is_sequence_on G by A15; :: thesis: verum