theorem Th22: :: COMPUT_1:23

for f being NAT * -defined to-naturals homogeneous Function holds
( ( f is len-total & not f is empty ) iff dom f = (arity f) -tuples_on NAT )