let G be Go-board; :: thesis: 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; :: thesis: 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); :: thesis: 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; :: 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, 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; :: thesis: verum