reconsider Z = 0 -tuples_on NAT as non empty Subset of (NAT * ) by Th13;
set f = Z --> 0 ;
A1: dom (Z --> 0 ) = Z by FUNCOP_1:19;
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 3 :: 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:110;
len x = 0 by A1, A4;
hence y in dom f by A1, A3, A5; :: thesis: verum

end;

take f ; :: thesis: ( not f is empty & f is homogeneous & f is to-naturals & f is len-total )
f is homogeneous

proof

thus dom f is with_common_domain by FUNCOP_1:19; :: according to UNIALG_1:def 1 :: thesis: verum

end;

hence ( not f is empty & f is homogeneous & f is to-naturals & f is len-total ) by A2; :: thesis: verum