let G be Go-board; for f being S-Sequence_in_R2
for p being Point of (TOP-REAL 2)
for k being Nat st 1 <= k & k < p .. f & f is_sequence_on G & p in rng f holds
( left_cell ((R_Cut (f,p)),k,G) = left_cell (f,k,G) & right_cell ((R_Cut (f,p)),k,G) = right_cell (f,k,G) )
let f be S-Sequence_in_R2; for p being Point of (TOP-REAL 2)
for k being Nat st 1 <= k & k < p .. f & f is_sequence_on G & p in rng f holds
( left_cell ((R_Cut (f,p)),k,G) = left_cell (f,k,G) & right_cell ((R_Cut (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 & p in rng f holds
( left_cell ((R_Cut (f,p)),k,G) = left_cell (f,k,G) & right_cell ((R_Cut (f,p)),k,G) = right_cell (f,k,G) )
let k be Nat; ( 1 <= k & k < p .. f & f is_sequence_on G & p in rng f implies ( left_cell ((R_Cut (f,p)),k,G) = left_cell (f,k,G) & right_cell ((R_Cut (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
and
A4:
p in rng f
; ( left_cell ((R_Cut (f,p)),k,G) = left_cell (f,k,G) & right_cell ((R_Cut (f,p)),k,G) = right_cell (f,k,G) )
A5: f | (p .. f) =
mid (f,1,(p .. f))
by A1, A2, FINSEQ_6:116, XXREAL_0:2
.=
R_Cut (f,p)
by A4, JORDAN1G:49
;
A6:
k + 1 <= p .. f
by A2, NAT_1:13;
p .. f <= len f
by A4, FINSEQ_4:21;
then
k + 1 <= len f
by A6, XXREAL_0:2;
hence
( left_cell ((R_Cut (f,p)),k,G) = left_cell (f,k,G) & right_cell ((R_Cut (f,p)),k,G) = right_cell (f,k,G) )
by A1, A3, A5, A6, GOBRD13:31; verum