let i, n be Element of NAT ; :: thesis: arity (n proj i) = n
consider d being object 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 Th35;
then A3: for x being FinSequence st x in dom (n proj i) holds
n = len x by CARD_1:def 7;
d in dom (n proj i) by A2;
hence arity (n proj i) = n by A3, MARGREL1:def 25; :: thesis: verum