@Michael – I think you've got into a bit of a muddle there by confusing composition of \$$\mathcal{V}\$$-functors with composition of \$$\mathcal{V}\$$-profunctors.

For the latter we want to define a \$$\Psi\Phi : \mathcal{X} \nrightarrow \mathcal{Z}\$$ for every pair \$$\Phi : \mathcal{X} \nrightarrow \mathcal{Y}\$$ and \$$\Psi : \mathcal{Y} \nrightarrow \mathcal{Z}\$$.

This amounts to defining a \$$\mathcal{V}\$$-functor \$$\Psi\Phi : \mathcal{X}^\text{op} \times \mathcal{Z} \to \mathcal{V}\$$ for every pair of \$$\mathcal{V}\$$-functors \$$\Phi : \mathcal{X}^\text{op} \times \mathcal{Y} \to \mathcal{V}\$$ and \$$\Psi : \mathcal{Y}^\text{op} \times \mathcal{Z} \to \mathcal{V}\$$.

So our "composite profunctor" is *not* a composite of \$$\mathcal{V}\$$-functors.

Instead we *define* it by writing down its value in \$$\mathcal{V}\$$ for any pair of objects \$$x \in \text{Ob}(\mathcal{X}^\text{op})\$$ and \$$z \in \text{Ob}(\mathcal{Z})\$$.

That's what this formula does:

$(\Psi\Phi)(x, z) = \bigvee\big(\Phi(x, y)\otimes\Psi(y, z)\big)$

Then we need to check that this definition is a \$$\mathcal{V}\$$-functor, which means proving

$(\mathcal{X}^\text{op}\times \mathcal{Z})((x, z), (x', z')) \leq \mathcal{V}(\Psi\Phi)(x, z), (\Psi\Phi)(x', z'))$

which in turn amounts to proving that

$\mathcal{X}(x', x) \otimes \mathcal{Z}(z, z') \leq (\Psi\Phi)(x, z)\multimap(\Psi\Phi)(x', z')$

which in turn amounts to proving that

$\mathcal{X}(x', x) \otimes \bigvee\big(\Phi(x, y)\otimes\Psi(y, z)\big) \otimes\mathcal{Z}(z, z') \leq \bigvee\big(\Phi(x', y)\otimes\Psi(y, z')\big)$

This is what we need to prove, and the trick here is to use the fact that \$$\otimes\$$ preserves joins.