Strengthening the hypotheses on $P$ and $Q$ from a fixed point *property* (every endofunction has *some* fixed point) to the existence of a fixed point *operator* $\mathsf{fix}$ with $$ \text{for any } f:P\to P, \qquad f({\mathsf{fix}}(f)) = {\mathsf{fix}}(f), $$ there is a standard theorem in **domain theory** or **lambda calculus** (theoretical computer science) due to **Hans Bekić**. We are given $h:P\times Q\to P\times Q$. Define $$ f = \lambda x.{\mathsf{fix}}_P(\lambda y.\pi_1(h(x,y))) : P\to Q $$ $$ g = \lambda y.{\mathsf{fix}}_Q(\lambda x.\pi_0(h(x,y))) : Q\to P $$ which have the properties that $$ f x = \pi_1(h(x,f x)) \quad\text{and}\quad g y = \pi_0(h(g y,y)). $$ Now let $x_0 = {\mathsf{fix}}_P(\lambda x.g(f x))$ and $y_0=f(x_0)$, so $x_0=g(y_0)$. Then $$ \pi_0(h(x_0,y_0)) = \pi_0(h(g y_0,y_0)) = g(y_0) = x_0 $$ $$ \pi_1(h(x_0,y_0)) = \pi_1(h(x_0,f x_0)) = f(x_0) = y_0 $$ so $(x_0,y_0)$ is a fixed point of $h$. In fact $f$ and $g$ are variables in this, so the argument provides a fixed point *operator* for $P\times Q$. Hans Bekić was a member of the IBM Vienna Laboratory but died in a mountain accident in 1982, leaving a lot of his work unpublished. It was edited and published by Cliff Jones and is available [here](http://homepages.cs.ncl.ac.uk/cliff.jones/publications/LNCS177-Bekic/), although I do not know exactly where the fixed point theorem is to be found in this.