set f = the Function of (n -tuples_on A),A;

A1: n in NAT by ORDINAL1:def 12;

then 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 A1, 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 A1, 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

A1: n in NAT by ORDINAL1:def 12;

then 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 A1, 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 A1, 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