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

proof

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

end;

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