dom (IncAddr F,k) = dom F by Def15;
hence dom (IncAddr F,k) c= NAT by RELAT_1:def 18; :: according to RELAT_1:def 18 :: thesis: verum