let m, n be Element of NAT ; :: thesis: arity (n const m) = n
set X = NAT ;
set d = the Element of n -tuples_on NAT;
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) ;
hence arity (n const m) = n by A2, MARGREL1:def 25; :: thesis: verum