MC-wff c= NAT * by Def7;
hence MC-wff is functional by FRAENKEL:17; :: thesis: