theorem :: JORDAN1J:48

for G being Go-board
for f, g being FinSequence of (TOP-REAL 2)
for k being 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) )