I am attempting to define direct products in the category **cont**(**mepfFcd**) (the category of monovalued, entirely defined continuous pointfree funcoids), see this draft article for a definition of this category.

A direct product of objects may possibly be defined as the cross-composition product (see this article).

A candidate for product of morphisms $latex f_1:\mathfrak{A}\rightarrow\mathfrak{B}$ and $latex f_2:\mathfrak{A}\rightarrow\mathfrak{C}$ of this category is the pointfree funcoid $latex f_1\times^{(D)} f_2$ defined by the formula:

\times^{\mathsf{FCD}} \langle f_2\rangle X \hspace{1em} |

\hspace{1em} X \in \mathrm{atoms}^{\mathfrak{A}} x

\right\}$.

The trouble is that I failed to prove that such a pointfree funcoid exists. So a conjecture:

**Conjecture** If $latex f_1$ and $latex f_2$ are monovalued, entirely defined funcoids then the pointfree funcoid defined by the above formula exists.