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 for b₁ being PartFunc of (X * ),X st b₁ = (n -tuples_on X) --> x holds
( not b₁ is empty & b₁ is quasi_total & b₁ is homogeneous ) by A1, COMPUT_1:25; :: thesis: verum