let G be Go-board; :: thesis: for f, g being FinSequence of (TOP-REAL 2)
for k being Element of NAT st 1 <= k & k < len f & f ^' g is_sequence_on G holds
( left_cell (f ^' g),k,G = left_cell f,k,G & right_cell (f ^' g),k,G = right_cell f,k,G )
let f, g be FinSequence of (TOP-REAL 2); :: thesis: for k being Element of NAT st 1 <= k & k < len f & f ^' g is_sequence_on G holds
( left_cell (f ^' g),k,G = left_cell f,k,G & right_cell (f ^' g),k,G = right_cell f,k,G )
let k be Element of NAT ; :: thesis: ( 1 <= k & k < len f & f ^' g is_sequence_on G implies ( left_cell (f ^' g),k,G = left_cell f,k,G & right_cell (f ^' g),k,G = right_cell f,k,G ) )
assume that
A1: 1 <= k and
A2: k < len f and
A3: f ^' g is_sequence_on G ; :: thesis: ( left_cell (f ^' g),k,G = left_cell f,k,G & right_cell (f ^' g),k,G = right_cell f,k,G )
A4: (f ^' g) | (len f) = f by Th50;
A5: k + 1 <= len f by A2, NAT_1:13;
len f <= len (f ^' g) by TOPREAL8:7;
then k + 1 <= len (f ^' g) by A5, XXREAL_0:2;
hence ( left_cell (f ^' g),k,G = left_cell f,k,G & right_cell (f ^' g),k,G = right_cell f,k,G ) by A1, A3, A4, A5, GOBRD13:32; :: thesis: verum