@Michael, @Anindya, thanks for the help! The second picture is even better than the previous one.

The problem is that in such "obvious" proofs everything is so obvious, that I don't even know how to formulate it and where it is better to start and how to end.

I immediately drew what one may see in [1](https://forum.azimuthproject.org/discussion/comment/20689/#Comment_20689), it a coarser version of @Michael drawings. It took me less than a minute to see **how** it works, the remaining question was **why** we prefer it to work in this way. @Anindya hinted to look into composition, and @John reminded that composition of morphisms works in this way in the product of categories **by definition**. And then in 17 @Anindya provided a perfect one-liner, thanks!
It reads like this to me: since \$$\otimes\$$ is a functor, it preseves composition, we use this fact to get to the 3rd equiality in 17, and then realize that composition in the source, product category, is a well defined process.