theorem Th35: :: REVROT_1:35

for f being constant standard special_circular_sequence
for p being Point of (TOP-REAL 2)
for k being Nat st p in rng f & 1 <= k & k < p .. f holds
left_cell (f,k) = left_cell ((Rotate (f,p)),((k + (len f)) -' (p .. f)))