theorem Th23: :: JORDAN1H:23

for k being Nat
for f being standard special_circular_sequence st 1 <= k & k + 1 <= len f holds
right_cell (f,k,(GoB f)) = right_cell (f,k)