set F = dom2tuple f;
dom (dom2tuple f) = 2 -tuples_on NAT by Def5;
hence dom (dom2tuple f) c= NAT * by FINSEQ_2:142; :: according to RELAT_1:def 18 :: thesis: verum