let n, i be Element of NAT ; :: thesis: arity (n proj i) = n
consider d being set such that
A1: d in n -tuples_on NAT by XBOOLE_0:def 1;
reconsider d = d as Element of n -tuples_on NAT by A1;
A2: dom (n proj i) = n -tuples_on NAT by Th40;
then A3: for x being FinSequence st x in dom (n proj i) holds
n = len x by FINSEQ_1:def 18;
d in dom (n proj i) by A2;
hence arity (n proj i) = n by A3, MARGREL1:def 26; :: thesis: verum