let n, m be Element of NAT ; :: thesis: arity (n const m) = n
set X = NAT ;
set d = the Element of n -tuples_on NAT;
A1: dom (n const m) = n -tuples_on NAT by FUNCOP_1:13;
then A2: for x being FinSequence st x in dom (n const m) holds
n = len x by CARD_1:def 7;
the Element of n -tuples_on NAT in dom (n const m) by A1;
hence arity (n const m) = n by A2, MARGREL1:def 25; :: thesis: verum