theorem :: DESCIP_1:11

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