Tensor product moments equal integration against the finite product measure

Each factor measure is finite, hence sigma-finite. Iterating [F2] constructs the finite product and makes it finite, with total mass equal to the product of the finite factor masses. For the product of intervals, the product sigma-algebra is the trace of the Euclidean Borel sigma-algebra: [F5] gives the binary Euclidean equality, and tracing its rectangle generators to the interval factors gives the corresponding trace equality; finite induction gives the $d$-factor case. Hence each coordinate monomial and its absolute value are product-measurable by [F5].

Fix an allowed multi-index $\alpha$. Apply [F3] successively to the nonnegative function ${\prod }_{j=1}^d\mathrm{\mid }{x}_j{\mathrm{\mid }}^{{\alpha }_j}$. At each step the inner one-variable integral is the finite absolute moment of the last coordinate, and it factors out as a nonnegative finite scalar. Induction therefore gives $\int {\prod }_j\mathrm{\mid }{x}_j{\mathrm{\mid }}^{{\alpha }_j}d\mu ={\prod }_j\int \mathrm{\mid }{x}_j{\mathrm{\mid }}^{{\alpha }_j}d{\mu }_j<\mathrm{\infty }$. Thus the signed real monomial is integrable.

Apply [F4] to that integrable monomial, integrating the last coordinate first. Its one-variable signed moment is $M_{{\alpha }_d}^{(d)}$; repeat for the preceding coordinates. Each use is legitimate by the absolute integrability in step 2.1, and finite induction yields $\int {\prod }_j{x}_j^{{\alpha }_j}d\mu ={\prod }_j{M}_{{\alpha }_j}^{(j)}$. At $d=1$ this is the moment definition itself.

A finite real linear combination of these integrable monomials is integrable by [F4]. Integrating that combination term by term in the fixed coefficient order from [F1] and substituting step 3.1 gives $\int Pd\mu ={\sum }_{\alpha }{c}_{\alpha }{\prod }_j{M}_{{\alpha }_j}^{(j)}=I_{\otimes }(P)$. No probability normalization or new choice assumption was used.