theorem Th33: :: REVROT_1:33

for p being Point of (TOP-REAL 2)
for f being circular FinSequence of (TOP-REAL 2) holds L~ (Rotate (f,p)) = L~ f