A product formula is proved which involves the unitary group generated by a semibounded self-adjoint operator and an orthogonal projection P. It gives a partial answer to the question about existence of the limit which describes quantum Zeno dynamics in the subspace Ran P.