A1: dom (n succ i) = n -tuples_on NAT by Def10;
n succ i is len-total

proof

let x, y be FinSequence of NAT ; :: according to COMPUT_1:def 3 :: thesis: ( len x = len y & x in dom (n succ i) implies y in dom (n succ i) )
assume A2: ( len x = len y & x in dom (n succ i) ) ; :: thesis: y in dom (n succ i)
then len x = n by A1, FINSEQ_1:def 18;
then y is Element of n -tuples_on NAT by A2, FINSEQ_2:110;
hence y in dom (n succ i) by A1; :: thesis: verum

end;

hence ( n succ i is len-total & not n succ i is empty ) by A1; :: thesis: verum