theorem Th53: :: JORDAN1J:53
for G being Go-board
for f being FinSequence of (TOP-REAL 2)
for p being Point of (TOP-REAL 2)
for k being Nat st 1 <= k & k < p .. f & f is_sequence_on G holds
( left_cell ((f -: p),k,G) = left_cell (f,k,G) & right_cell ((f -: p),k,G) = right_cell (f,k,G) )