for D being non empty set
for s being FinSequence of D st 1 <= len s holds
Op-Shift (s,(- (len s))) = s