dom (dom2tuple f) = 2 -tuples_on D by Def5;
hence dom2tuple f is homogeneous by COMPUT_1:16; :: thesis: verum