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