:: deftheorem Def7 defines succ COMPUT_1:def 7 :
for n, i being Element of NAT
for b₃ being NAT * -defined to-naturals homogeneous Function holds
( b₃ = n succ i iff ( dom b₃ = n -tuples_on NAT & ( for p being Element of n -tuples_on NAT holds b₃ . p = (p /. i) + 1 ) ) );