theorem :: DESCIP_1:10

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