for D being non empty set
for p1, p2 being Element of D
for f being FinSequence of D st f is circular & f just_once_values p2 holds
Rotate ((Rotate (f,p1)),p2) = Rotate (f,p2)