theorem Th9: :: COMPUT_1:9

for i, n being Nat
for D being non empty set st 1 <= i & i <= n + 1 holds
for p being Element of (n + 1) -tuples_on D holds Del (p,i) in n -tuples_on D