Finite axiomatization of $\mathbf{\text{GL}}\times \mathbf{\text{S5}}$ and $\mathbf{\text{Grz}}\times \mathbf{\text{S5}}$

We prove that $\mathbf{G}\mathbf{L}\times \mathbf{S}\mathbf{5}$ is product matching, and that $\mathbf{G}\mathbf{r}\mathbf{z}\times \mathbf{S}\mathbf{5}$ is axiomatizable by adding to $[\mathbf{G}\mathbf{r}\mathbf{z},\mathbf{S}\mathbf{5}]$ the Gödel translation of the monadic Casari formula. This settles the question of the finite axiomatizability of these logics posed by Gabbay and Shehtman (1998).