set X = NAT ;
set f = (n -tuples_on NAT) --> m;
A1: n -tuples_on NAT c= NAT * by FINSEQ_2:142;
A2: dom ((n -tuples_on NAT) --> m) = n -tuples_on NAT by FUNCOP_1:13;
(n -tuples_on NAT) --> m is homogeneous

proof

thus dom ((n -tuples_on NAT) --> m) is with_common_domain ; :: according to MARGREL1:def 21 :: thesis: verum

end;

hence (n -tuples_on NAT) --> m is NAT * -defined to-naturals homogeneous Function by A1, A2, RELAT_1:def 18; :: thesis: verum