:: deftheorem defines const COMPUT_1:def 6 :
for n, m being Nat holds n const m = (n -tuples_on NAT) --> m;