Description: Extend the definition of a wff to include the function predicate with domain and codomain. (Read: F maps A into B .)