let G be Go-board; 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); 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); ( 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
; 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 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).| = 1let n be
Nat;
( 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*>
;
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).| = 1A8:
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;
verum end;
now 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;
( [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*>
;
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
;
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 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;
( n in dom (f ^ <*p*>) implies ex i, j being Nat st
( [j,b3] in Indices G & (f ^ <*p*>) /. i = G * (j,b3) ) )assume A16:
n in dom (f ^ <*p*>)
;
ex i, j being Nat st
( [j,b3] in Indices G & (f ^ <*p*>) /. i = G * (j,b3) )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
;
ex i, j being Nat st
( [j,b3] in Indices G & (f ^ <*p*>) /. i = G * (j,b3) )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;
ex j being Nat st
( [i,j] in Indices G & (f ^ <*p*>) /. n = G * (i,j) )take j =
j;
( [i,j] in Indices G & (f ^ <*p*>) /. n = G * (i,j) )thus
[i,j] in Indices G
by A18;
(f ^ <*p*>) /. n = G * (i,j)thus
(f ^ <*p*>) /. n = G * (
i,
j)
by A17, A19, FINSEQ_4:68;
verum end; suppose
ex
l being
Nat st
(
l in dom <*p*> &
n = (len f) + l )
;
ex i, j being Nat st
( [j,b3] in Indices G & (f ^ <*p*>) /. i = G * (j,b3) )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;
ex j being Nat st
( [i,j] in Indices G & (f ^ <*p*>) /. n = G * (i,j) )take j =
j;
( [i,j] in Indices G & (f ^ <*p*>) /. n = G * (i,j) )thus
[i,j] in Indices G
by A22;
(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;
verum end; end; end;
hence
f ^ <*p*> is_sequence_on G
by A15; verum