theorem Th1: :: DESCIP_1:1

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