let n, m be Element of NAT ; :: thesis: arity (n const m) = n
set X = NAT ;
consider d being Element of n -tuples_on NAT ;
A1: dom (n const m) = n -tuples_on NAT by FUNCOP_1:19;
then A2: for x being FinSequence st x in dom (n const m) holds
n = len x by FINSEQ_1:def 18;
d in dom (n const m) by A1;
hence arity (n const m) = n by A2, MARGREL1:def 26; :: thesis: verum