theorem Th14: :: DESCIP_1:14

for D being non empty set
for n being non zero Element of NAT
for m being Integer
for s being Element of n -tuples_on D holds Op-Shift (s,m) is Element of n -tuples_on D