# A new proposition about infimum product

I’ve proved a new simple proposition about infimum product:

Theorem
Let $\pi^X_i$ be metamonovalued morphisms. If $S \in \mathscr{P} ( \mathsf{FCD} ( A_0 ; B_0) \times \mathsf{FCD} ( A_1 ; B_1))$
for some sets $A_0$, $B_0$, $A_1$, $B_1$ then
$\bigsqcap \left\{ a \times b \,|\, ( a ; b) \in S \right\} = \bigsqcap \mathrm{dom}\, S \times \bigsqcap \mathrm{im}\, S.$

And its corollary:

$( a_0 \times b_0) \sqcap ( a_1 \times b_1) = ( a_0 \sqcap a_1) \times ( b_0 \sqcap b_1)$.

See this online article (here there is also the dual of the above statements).