  Given a nonnegative self-adjoint operator $H$ acting on a separable Hilbert
space and an orthogonal projection $P$ such that $H_P :=
(H^{1/2}P)^*(H^{1/2}P)$ is densely defined, we prove that $\lim_{n\rightarrow
\infty} (P\,\mathrm{e}^{-itH/n}P)^n = \mathrm{e}^{-itH_P}P$ holds in the strong
operator topology. We also derive modifications of this product formula and its
extension to the situation when $P$ is replaced by a strongly continuous
projection-valued function satisfying $P(0)=P$.
