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