reconsider Z = 0 -tuples_on NAT as non empty Subset of (NAT *) by FINSEQ_2:90;
set f = Z --> 0;
reconsider f = Z --> 0 as NAT * -defined Function ;
A2: f is len-total
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
A3: len x = len y and
A4: x in dom f ; :: thesis: y in dom f
A5: y is Element of (len y) -tuples_on NAT by FINSEQ_2:92;
len x = 0 by A4;
hence y in dom f by A3, A5; :: thesis: verum
end;
take f ; :: thesis: ( not f is empty & f is homogeneous & f is to-naturals & f is len-total )
thus ( not f is empty & f is homogeneous & f is to-naturals & f is len-total ) by A2; :: thesis: verum