reconsider Z = 0 -tuples_on NAT as non empty Subset of (NAT * ) by Th13;
set f = Z --> 0 ;
A1: ( dom (Z --> 0 ) = Z & rng (Z --> 0 ) c= {0 } ) by FUNCOP_1:19;
reconsider f = Z --> 0 as NAT * -defined Function ;
take f ; :: thesis: ( not f is empty & f is homogeneous & f is to-naturals & f is len-total )
A2: f is homogeneous

proof

let x, y be FinSequence; :: according to UNIALG_1:def 1 :: thesis: ( not x in dom f or not y in dom f or len x = len y )
assume ( x in dom f & y in dom f ) ; :: thesis: len x = len y
then ( len x = 0 & len y = 0 ) by A1, FINSEQ_1:def 18;
hence len x = len y ; :: thesis: verum

end;

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
A4: len x = len y and
A5: x in dom f ; :: thesis: y in dom f
A6: y is Element of (len y) -tuples_on NAT by FINSEQ_2:110;
len x = 0 by A1, A5, FINSEQ_1:def 18;
hence y in dom f by A1, A4, A6; :: thesis: verum

end;

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