set X = NAT ;
set f = (n -tuples_on NAT) --> m;
A1: n -tuples_on NAT c= NAT * by FINSEQ_2:142;
(n -tuples_on NAT) --> m is homogeneous ;
hence (n -tuples_on NAT) --> m is NAT * -defined to-naturals homogeneous Function by A1, RELAT_1:def 18; :: thesis: verum