set f = the Function of (n -tuples_on A),A;
n -tuples_on A c= A * by FINSEQ_2:134;
then reconsider f = the Function of (n -tuples_on A),A as PartFunc of (A *),A by RELSET_1:7;
A2: dom f = n -tuples_on A by FUNCT_2:def 1;
then reconsider f = f as homogeneous PartFunc of (A *),A by COMPUT_1:16;
set t = the Element of n -tuples_on A;
A3: arity f = len the Element of n -tuples_on A by A2, MARGREL1:def 25
.= n by FINSEQ_2:133 ;
then reconsider f = f as non empty homogeneous quasi_total PartFunc of (A *),A by A2, COMPUT_1:22;
take f ; :: thesis: f is n -ary
thus f is n -ary by A3, COMPUT_1:def 21; :: thesis: verum