reconsider m = n as Element of NAT by ORDINAL1:def 12;
set f = (n -tuples_on X) --> x;
A1:
dom ((n -tuples_on X) --> x) = m -tuples_on X
by FUNCOP_1:13;
then reconsider f = (n -tuples_on X) --> x as non empty homogeneous PartFunc of (X *),X by COMPUT_1:16;
arity f = m
by A1, COMPUT_1:24;
hence
for b1 being PartFunc of (X *),X st b1 = (n -tuples_on X) --> x holds
( not b1 is empty & b1 is quasi_total & b1 is homogeneous )
by A1, COMPUT_1:22; verum