dom H₃(f) = 1 -tuples_on (dom f) by Def4;
hence not dom2tuple f is empty ; :: thesis: verum