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