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
; f is n -ary
thus
f is n -ary
by A3, COMPUT_1:def 21; verum