A1: dom (n proj i) = n -tuples_on NAT by Th40;
n proj 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 proj i) implies y in dom (n proj i) )
assume that
A2: len x = len y and
A3: x in dom (n proj i) ; :: thesis: y in dom (n proj i)
len x = n by A1, A3, FINSEQ_1:def 18;
then y is Element of n -tuples_on NAT by A2, FINSEQ_2:110;
hence y in dom (n proj i) by A1; :: thesis: verum

end;

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