Oh, they're certainly not easy to derive. The fact that Wick products give densely defined operators was first proved by Jaffe in 1966 . However I personally fined a later derivation by Segal in 1967 to be much clearer . Segal has a very erudite way of writing, which you will either love or find very difficult to read.
I should also say the theorem is much harder to prove in the Hamiltonian approach that I'm discussing. In the Functional-Integral (Path-Integral) approach it's just a matter of evaluating a single Feynman diagram. See Glimm and Jaffe's book Section 8.5, Proposition 8.5.1.
 Jaffe, A. : Wick polynomials at a fixed time. J. Math. Phys. 7
, 1250 — 1255
 Segal, I. "Notes toward the construction of nonlinear relativistic quantum
fields, I. The Hamiltonian in two space-time dimensions as the generator
of a C*-automorphism group." Proc. Natl. Acad. Sci. U. S. 57
You're more than welcome, I will be glad to continue the series of posts.