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