let G be Go-board; for f being FinSequence of (TOP-REAL 2)
for p being Point of (TOP-REAL 2)
for k being Nat st 1 <= k & k < p .. f & f is_sequence_on G holds
( left_cell ((f -: p),k,G) = left_cell (f,k,G) & right_cell ((f -: p),k,G) = right_cell (f,k,G) )
let f be FinSequence of (TOP-REAL 2); for p being Point of (TOP-REAL 2)
for k being Nat st 1 <= k & k < p .. f & f is_sequence_on G holds
( left_cell ((f -: p),k,G) = left_cell (f,k,G) & right_cell ((f -: p),k,G) = right_cell (f,k,G) )
let p be Point of (TOP-REAL 2); for k being Nat st 1 <= k & k < p .. f & f is_sequence_on G holds
( left_cell ((f -: p),k,G) = left_cell (f,k,G) & right_cell ((f -: p),k,G) = right_cell (f,k,G) )
let k be Nat; ( 1 <= k & k < p .. f & f is_sequence_on G implies ( left_cell ((f -: p),k,G) = left_cell (f,k,G) & right_cell ((f -: p),k,G) = right_cell (f,k,G) ) )
assume that
A1:
1 <= k
and
A2:
k < p .. f
and
A3:
f is_sequence_on G
; ( left_cell ((f -: p),k,G) = left_cell (f,k,G) & right_cell ((f -: p),k,G) = right_cell (f,k,G) )
A4:
k + 1 <= p .. f
by A2, NAT_1:13;
A5:
f | (p .. f) = f -: p
by FINSEQ_5:def 1;
per cases
( p in rng f or p .. f = 0 )
by TOPREAL8:4;
suppose
p in rng f
;
( left_cell ((f -: p),k,G) = left_cell (f,k,G) & right_cell ((f -: p),k,G) = right_cell (f,k,G) )then
p .. f <= len f
by FINSEQ_4:21;
then
k + 1
<= len f
by A4, XXREAL_0:2;
hence
(
left_cell (
(f -: p),
k,
G)
= left_cell (
f,
k,
G) &
right_cell (
(f -: p),
k,
G)
= right_cell (
f,
k,
G) )
by A1, A3, A5, A4, GOBRD13:31;
verum end;