theorem Th5: :: SRINGS_5:5

for n being Nat
for D being non empty set
for D1 being non empty Subset of D holds n -tuples_on D1 c= n -tuples_on D