let k, n be Nat; for f being FinSequence of (TOP-REAL 2)
for G being Go-board st 1 <= k & k + 1 <= len (f /^ n) & n <= len f & f is_sequence_on G holds
( left_cell (f,(k + n),G) = left_cell ((f /^ n),k,G) & right_cell (f,(k + n),G) = right_cell ((f /^ n),k,G) )
let f be FinSequence of (TOP-REAL 2); for G being Go-board st 1 <= k & k + 1 <= len (f /^ n) & n <= len f & f is_sequence_on G holds
( left_cell (f,(k + n),G) = left_cell ((f /^ n),k,G) & right_cell (f,(k + n),G) = right_cell ((f /^ n),k,G) )
let G be Go-board; ( 1 <= k & k + 1 <= len (f /^ n) & n <= len f & f is_sequence_on G implies ( left_cell (f,(k + n),G) = left_cell ((f /^ n),k,G) & right_cell (f,(k + n),G) = right_cell ((f /^ n),k,G) ) )
set g = f /^ n;
assume that
A1:
1 <= k
and
A2:
k + 1 <= len (f /^ n)
and
A3:
n <= len f
and
A4:
f is_sequence_on G
; ( left_cell (f,(k + n),G) = left_cell ((f /^ n),k,G) & right_cell (f,(k + n),G) = right_cell ((f /^ n),k,G) )
A5:
( len (f /^ n) = (len f) - n & (k + 1) + n <= (len (f /^ n)) + n )
by A2, A3, RFINSEQ:def 1, XREAL_1:6;
k in dom (f /^ n)
by A1, A2, SEQ_4:134;
then A6:
(f /^ n) /. k = f /. (k + n)
by FINSEQ_5:27;
set lf = left_cell (f,(k + n),G);
set lfn = left_cell ((f /^ n),k,G);
set rf = right_cell (f,(k + n),G);
set rfn = right_cell ((f /^ n),k,G);
A7:
( (k + 1) + n = (k + n) + 1 & 1 <= k + n )
by A1, NAT_1:12;
k + 1 in dom (f /^ n)
by A1, A2, SEQ_4:134;
then A8:
(f /^ n) /. (k + 1) = f /. ((k + 1) + n)
by FINSEQ_5:27;
A9:
f /^ n is_sequence_on G
by A4, JORDAN8:2;
then consider i1, j1, i2, j2 being Nat such that
A10:
( [i1,j1] in Indices G & (f /^ n) /. k = G * (i1,j1) & [i2,j2] in Indices G & (f /^ n) /. (k + 1) = G * (i2,j2) )
and
A11:
( ( i1 = i2 & j1 + 1 = j2 ) or ( i1 + 1 = i2 & j1 = j2 ) or ( i1 = i2 + 1 & j1 = j2 ) or ( i1 = i2 & j1 = j2 + 1 ) )
by A1, A2, JORDAN8:3;
A12:
( j1 + 1 > j1 & j2 + 1 > j2 )
by NAT_1:13;
A13:
( i1 + 1 > i1 & i2 + 1 > i2 )
by NAT_1:13;
now ( left_cell (f,(k + n),G) = left_cell ((f /^ n),k,G) & right_cell (f,(k + n),G) = right_cell ((f /^ n),k,G) )per cases
( ( i1 = i2 & j1 + 1 = j2 ) or ( i1 + 1 = i2 & j1 = j2 ) or ( i1 = i2 + 1 & j1 = j2 ) or ( i1 = i2 & j1 = j2 + 1 ) )
by A11;
suppose A14:
(
i1 = i2 &
j1 + 1
= j2 )
;
( left_cell (f,(k + n),G) = left_cell ((f /^ n),k,G) & right_cell (f,(k + n),G) = right_cell ((f /^ n),k,G) )hence left_cell (
f,
(k + n),
G) =
cell (
G,
(i1 -' 1),
j1)
by A4, A10, A12, A6, A8, A5, A7, Def2
.=
left_cell (
(f /^ n),
k,
G)
by A1, A2, A9, A10, A12, A14, Def2
;
right_cell (f,(k + n),G) = right_cell ((f /^ n),k,G)thus right_cell (
f,
(k + n),
G) =
cell (
G,
i1,
j1)
by A4, A10, A12, A6, A8, A5, A7, A14, Def1
.=
right_cell (
(f /^ n),
k,
G)
by A1, A2, A9, A10, A12, A14, Def1
;
verum end; suppose A15:
(
i1 + 1
= i2 &
j1 = j2 )
;
( left_cell (f,(k + n),G) = left_cell ((f /^ n),k,G) & right_cell (f,(k + n),G) = right_cell ((f /^ n),k,G) )hence left_cell (
f,
(k + n),
G) =
cell (
G,
i1,
j1)
by A4, A10, A13, A6, A8, A5, A7, Def2
.=
left_cell (
(f /^ n),
k,
G)
by A1, A2, A9, A10, A13, A15, Def2
;
right_cell (f,(k + n),G) = right_cell ((f /^ n),k,G)thus right_cell (
f,
(k + n),
G) =
cell (
G,
i1,
(j1 -' 1))
by A4, A10, A13, A6, A8, A5, A7, A15, Def1
.=
right_cell (
(f /^ n),
k,
G)
by A1, A2, A9, A10, A13, A15, Def1
;
verum end; suppose A16:
(
i1 = i2 + 1 &
j1 = j2 )
;
( left_cell (f,(k + n),G) = left_cell ((f /^ n),k,G) & right_cell (f,(k + n),G) = right_cell ((f /^ n),k,G) )hence left_cell (
f,
(k + n),
G) =
cell (
G,
i2,
(j2 -' 1))
by A4, A10, A13, A6, A8, A5, A7, Def2
.=
left_cell (
(f /^ n),
k,
G)
by A1, A2, A9, A10, A13, A16, Def2
;
right_cell (f,(k + n),G) = right_cell ((f /^ n),k,G)thus right_cell (
f,
(k + n),
G) =
cell (
G,
i2,
j2)
by A4, A10, A13, A6, A8, A5, A7, A16, Def1
.=
right_cell (
(f /^ n),
k,
G)
by A1, A2, A9, A10, A13, A16, Def1
;
verum end; suppose A17:
(
i1 = i2 &
j1 = j2 + 1 )
;
( left_cell (f,(k + n),G) = left_cell ((f /^ n),k,G) & right_cell (f,(k + n),G) = right_cell ((f /^ n),k,G) )hence left_cell (
f,
(k + n),
G) =
cell (
G,
i1,
j2)
by A4, A10, A12, A6, A8, A5, A7, Def2
.=
left_cell (
(f /^ n),
k,
G)
by A1, A2, A9, A10, A12, A17, Def2
;
right_cell (f,(k + n),G) = right_cell ((f /^ n),k,G)thus right_cell (
f,
(k + n),
G) =
cell (
G,
(i1 -' 1),
j2)
by A4, A10, A12, A6, A8, A5, A7, A17, Def1
.=
right_cell (
(f /^ n),
k,
G)
by A1, A2, A9, A10, A12, A17, Def1
;
verum end; end; end;
hence
( left_cell (f,(k + n),G) = left_cell ((f /^ n),k,G) & right_cell (f,(k + n),G) = right_cell ((f /^ n),k,G) )
; verum