dom F c= NAT by RELAT_1:def 18;
hence dom F is natural-membered ; :: thesis: verum