:: deftheorem defines doms HILB10_7:def 14 :
for n, k being Nat holds doms (n,k) = k -tuples_on (Seg n);