for s being FinSequence st 1 <= len s holds
len (Op-LeftShift s) = len s