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 and of this category is the pointfree funcoid defined by the formula:

.

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

Conjecture If and are monovalued, entirely defined funcoids then the pointfree funcoid defined by the above formula exists.