set F = dom2tuple f;
A1: dom2tuple f is Relation of (D *),D by Th30;
A2: dom (dom2tuple f) = 1 -tuples_on (dom f) by Def4;
dom f = D by FUNCT_2:def 1;
hence arity (dom2tuple f) = 1 by A1, A2, COMPUT_1:25; :: according to COMPUT_1:def 21 :: thesis: verum