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 0 -ary
thus arity ((0 -tuples_on X) --> the Element of X) = 0 by Th2; :: according to COMPUT_1:def 21 :: thesis: verum