let G be Go-board; :: thesis: for f being S-Sequence_in_R2
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 & 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; :: 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 & 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); :: thesis: for k being Element of 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 Element of NAT ; :: thesis: ( 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 ; :: thesis: ( 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, JORDAN3:25, XXREAL_0:2
.= R_Cut f,p by A4, JORDAN1G:57 ;
A6: k + 1 <= p .. f by A2, NAT_1:13;
p .. f <= len f by A4, FINSEQ_4:31;
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:32; :: thesis: verum