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 Th20;

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 f9 = f as non empty homogeneous quasi_total PartFunc of (NAT *),NAT by Th16;
consider x being object such that
A2: x in dom f9 by XBOOLE_0:def 1;
reconsider x9 = x as FinSequence of NAT by A2, FINSEQ_1:def 11;
A3: len x9 = arity f by A2, MARGREL1:def 25;

now :: thesis: for z being object holds
( ( z in dom f implies z in (arity f) -tuples_on NAT ) & ( z in (arity f) -tuples_on NAT implies z in dom f ) )

let z be object ; :: 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 z9 = z as Element of (arity f) -tuples_on NAT ;
len z9 = arity f by CARD_1:def 7;
hence z in dom f by A2, A3, MARGREL1:def 22; :: thesis: verum

end;

hence dom f = (arity f) -tuples_on NAT ; :: 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 2 :: thesis: ( len x = len y & x in dom f implies y in dom f )
assume that
A5: len x = len y and
A6: x in dom f ; :: thesis: y in dom f
len x = arity f by A4, A6, CARD_1:def 7;
then y is Element of (arity f) -tuples_on NAT by A5, FINSEQ_2:92;
hence y in dom f by A4; :: thesis: verum

end;

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