:: deftheorem defines Op-RightShift DESCIP_1:def 2 :
for s being FinSequence holds Op-RightShift s = (<*(s . (len s))*> ^ s) | (len s);