let n, i be Element of NAT ; :: thesis: arity (n succ i) = n
consider d being set 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, Def10;
dom (n succ i) = n -tuples_on NAT by Def10;
then A2: for y being FinSequence st y in dom (n succ i) holds
n = len y by FINSEQ_1:def 18;
d in dom (n succ i) by A1;
hence arity (n succ i) = n by A2, UNIALG_1:def 10; :: thesis: verum