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

wff F : A --> B