Projections are introduced using the definite description operator on these predicates :
![\begin{definition}[]~
\begin{center}%
\afdmath{}\text{\rm fstP}\hspace{0.2em} \t...
...
\SaveVerb{Verb}fstP z x\marginpar{\UseVerb{Verb}}\end{center}\end{definition}](img110.png)
![\begin{definition}[]~
\begin{center}%
\afdmath{}\text{\rm sndP}\hspace{0.2em} \t...
...
\SaveVerb{Verb}sndP z y\marginpar{\UseVerb{Verb}}\end{center}\end{definition}](img111.png)
![\begin{definition}[ projections defined as functions ]\hspace{1cm}
\begin{itemiz...
...}
\SaveVerb{Verb}snd z\marginpar{\UseVerb{Verb}}
\end{itemize}\end{definition}](img112.png)
Then using the properties of the definite description, we prove the following facts.
![\begin{fact}[%
\afdmath{}\text{\rm fst}.\text{\rm Product}\endafdmath{}]property...
...3em}{2.em}
\text{\it x}\endprettybox{}\endprettybox{}\endafdmmath{}
\end{fact}](img113.png){kind=small}
![\begin{fact}[%
\afdmath{}\text{\rm snd}.\text{\rm Product}\endafdmath{}]property...
...3em}{2.em}
\text{\it y}\endprettybox{}\endprettybox{}\endafdmmath{}
\end{fact}](img114.png){kind=small}
We add these propositions as rewriting rules and we close the definition of fst and snd
fst.Product added as equation
snd.Product added as equation
![\begin{definition}[]~
\begin{center}List of theorems: calcul.Product := fst.Product snd.Product
\end{center}\end{definition}](img115.png){kind=small}
We also prove the following propositions :
fst.total.Product added as introduction rule (abbrev: fst , options: -t )
snd.total.Product added as introduction rule (abbrev: snd , options: -t )
![\begin{fact}[%
\afdmath{}\text{\rm surjective}.\text{\rm Product}\endafdmath{}]R...
...3em}{2.em}
\text{\it x}\endprettybox{}\endprettybox{}\endafdmmath{}
\end{fact}](img118.png)
surjective.Product added as equation
The two first are added as totality rule and the last one is added as rewriting rule