let i, n be Nat; :: thesis: arity (n succ i) = n
consider d being object such that
A1: d in dom (n succ i) by XBOOLE_0:def 1;
reconsider d = d as Element of n -tuples_on NAT by A1, Def7;
dom (n succ i) = n -tuples_on NAT by Def7;
then A2: for y being FinSequence st y in dom (n succ i) holds
n = len y by CARD_1:def 7;
d in dom (n succ i) by A1;
hence arity (n succ i) = n by A2, MARGREL1:def 25; :: thesis: verum