reconsider m = n as Element of NAT by ORDINAL1:def 13;
set f = (n -tuples_on X) --> x;
A1: ( m -tuples_on X c= X * & rng ((n -tuples_on X) --> x) c= X & dom ((n -tuples_on X) --> x) = m -tuples_on X ) by CATALG_1:6, FUNCOP_1:19;
then reconsider f = (n -tuples_on X) --> x as non empty homogeneous PartFunc of X * ,X by COMPUT_1:19;
arity f = m by A1, COMPUT_1:27;
hence (n -tuples_on X) --> x is non empty homogeneous quasi_total PartFunc of X * ,X by A1, COMPUT_1:25; :: thesis: verum