for Y being set
for m being Nat holds (m + 1) -tuples_on Y c= (Y *) \ {{}}