let f be NAT * -defined to-naturals homogeneous Function; :: thesis: ( ( f is len-total & not f is empty ) iff dom f = (arity f) -tuples_on NAT )
A1: dom f c= (arity f) -tuples_on NAT by Th24;

hereby :: thesis: ( dom f = (arity f) -tuples_on NAT implies ( f is len-total & not f is empty ) )

assume ( f is len-total & not f is empty ) ; :: thesis: dom f = (arity f) -tuples_on NAT
then reconsider f' = f as non empty homogeneous quasi_total PartFunc of (NAT * ),NAT by Th20;
consider x being set such that
A2: x in dom f' by XBOOLE_0:def 1;
reconsider x' = x as FinSequence of NAT by A2, FINSEQ_1:def 11;
A3: len x' = arity f by A2, UNIALG_1:def 10;

now

let z be set ; :: thesis: ( ( z in dom f implies z in (arity f) -tuples_on NAT ) & ( z in (arity f) -tuples_on NAT implies z in dom f ) )
thus ( z in dom f implies z in (arity f) -tuples_on NAT ) by A1; :: thesis: ( z in (arity f) -tuples_on NAT implies z in dom f )
assume z in (arity f) -tuples_on NAT ; :: thesis: z in dom f
then reconsider z' = z as Element of (arity f) -tuples_on NAT ;
len z' = arity f by FINSEQ_1:def 18;
hence z in dom f by A2, A3, UNIALG_1:def 2; :: thesis: verum

end;

hence dom f = (arity f) -tuples_on NAT by TARSKI:2; :: thesis: verum

end;

assume A4: dom f = (arity f) -tuples_on NAT ; :: thesis: ( f is len-total & not f is empty )
thus f is len-total :: thesis: not f is empty

proof

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

end;

thus not f is empty by A4; :: thesis: verum