To define the product of two predicates, we extend the language with one binary function symbol [ x, y ] . Then the product of two unary predicates is defined by the following predicate A × B
![\begin{definition}[ Product ]\hspace{1cm}
\begin{itemize}
\item product['a,'b]
\...
...erb{Verb}Product A B p\marginpar{\UseVerb{Verb}}
\end{itemize}\end{definition}](img105.png)
![\begin{fact}[%
\afdmath{}\text{\rm intro}.\text{\rm Product}\endafdmath{}]Produc...
...;\;
\text{\it y}\right)\endprettybox{}\endprettybox{}\endafdmmath{}
\end{fact}](img106.png){kind=small}
intro.Product added as introduction rule (abbrev: i , options: -i -c )
![\begin{fact}[%
\afdmath{}\text{\rm elim}.\text{\rm Product}\endafdmath{}]Product...
...reak{0.36em}{2.em}
\text{\it X}\right)\endprettybox{}\endafdmmath{}
\end{fact}](img107.png){kind=small}
elim.Product added as elimination rule (abbrev: r , options: -i )
![\begin{axiom}[%
\afdmath{}\text{\rm injective}.\text{\rm Product}\endafdmath{}]P...
...'\endprettybox{}\endprettybox{}\right)\endprettybox{}\endafdmmath{}
\end{axiom}](img108.png){kind=small}
injective_left.Product added as elimination rule (abbrev: Product , options: -i -n )