set F = dom2tuple f;
A1: dom2tuple f is Relation of (D *),D by Th31;
dom (dom2tuple f) = 2 -tuples_on D by Def5;
hence arity (dom2tuple f) = 2 by A1, COMPUT_1:25; :: according to COMPUT_1:def 21 :: thesis: verum