let G be Go-board; :: thesis: for f being FinSequence of (TOP-REAL 2)
for p being Point of (TOP-REAL 2)
for k being Element of 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); :: thesis: for p being Point of (TOP-REAL 2)
for k being Element of 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); :: thesis: for k being Element of 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 Element of NAT ; :: thesis: ( 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
; :: thesis: ( left_cell (f -: p),k,G = left_cell f,k,G & right_cell (f -: p),k,G = right_cell f,k,G )
A4:
f | (p .. f) = f -: p
by FINSEQ_5:def 1;
A5:
k + 1 <= p .. f
by A2, NAT_1:13;
per cases
( p in rng f or p .. f = 0 )
by TOPREAL8:4;
suppose
p in rng f
;
:: thesis: ( 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:31;
then
k + 1
<= len f
by A5, 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, A4, A5, GOBRD13:32;
:: thesis: verum end;