theorem :: DESCIP_1:16

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