theorem :: DESCIP_1:9

for D being non empty set
for n being non zero Element of NAT
for s being Element of n -tuples_on D holds Op-RightShift s is Element of n -tuples_on D