set x = the Element of X;
set f = (0 -tuples_on X) --> the Element of X;
take (0 -tuples_on X) --> the Element of X ; :: thesis: (0 -tuples_on X) --> the Element of X is nullary
thus arity ((0 -tuples_on X) --> the Element of X) = 0 by Th2; :: according to COMPUT_1:def 24 :: thesis: verum