for s being FinSequence holds len (Op-RightShift s) = len s