Perturbative renormalization of composite operators via flow equations II: Short distance expansion

We give a rigorous and very detailed derivation of the short distance expansion for a product of two arbitrary composite operators in the framework of the perturbative Euclidean massive Φ₄⁴. The technically almost trivial proof rests on an extension of the differential flow equation method to Green functions with bilocal insertions, for which we also establish a set of generalized Zimmermann identities and Lowenstein rules.