HP-WFF c= NAT * by Def5;
hence HP-WFF is functional by FRAENKEL:17; :: thesis: verum