for D being non empty set
for n, m being non zero Element of NAT
for r being Element of n -tuples_on D st m <= n & 8 <= n - m holds
Op-Left ((Op-Right (r,m)),8) is Element of 8 -tuples_on D