Step 0 (Integrals with respect to the restriction of P to T). Let PT denote the restriction of P to T; it is a measure on (Ω,T) with PT(Ω)=1, countable additivity for members of T being a special case of that for members of F, so (Ω,T,PT) is a finite, hence σ-finite, measure space. We claim that for every T-measurable Ξ:Ω→[0,∞],
∫ΩΞdPT=∫ΩΞdP=E[Ξ]in [0,∞].(0)
For m≥1 let sm=∑p=1m2m2−m1{Ξ≥p2−m}, where 1{⋯} is the indicator of the event in braces. Each sm is a nonnegative simple function on (Ω,T), the sets {Ξ≥p2−m}=⋂n{Ξ>p2−m−1/n} lying in T, and its integral with respect to PT and with respect to P is the same number, the integral of a nonnegative simple function being computed from the measures of the level sets of its standard representation, which are members of T on which PT and P agree. At every ω: sm(ω)=2−mmin(m2m,⌊2mΞ(ω)⌋) when Ξ(ω)<∞, with ⌊⋅⌋ the integer part, since p≤2mΞ(ω) holds for exactly min(m2m,⌊2mΞ(ω)⌋) indices p∈{1,…,m2m}, and sm(ω)=m when Ξ(ω)=∞. Hence the sequence (sm(ω))m is nondecreasing (from 2⌊y⌋≤⌊2y⌋, which holds because 2⌊y⌋ is an integer at most 2y and every integer n≤x satisfies n≤⌊x⌋, as n≥⌊x⌋+1 would give n>x; and from the growth of the cap m) and converges to Ξ(ω) (for Ξ(ω)<∞ and m≥Ξ(ω) one has Ξ(ω)−2−m≤sm(ω)≤Ξ(ω); for Ξ(ω)=∞, sm(ω)=m→∞). The monotone convergence theorem, applied on (Ω,T,PT) and on (Ω,F,P) (where sm and Ξ are also measurable, as T⊆F), gives (0), both sides being the supremum of the same sequence of numbers.
Step 1 (The pairing map). Let Φ:Ω→R×Ω, Φ(ω)=(W(ω),ω). For a measurable rectangle A×C with A∈R and C∈T, Φ−1(A×C)=W−1(A)∩C∈F. Since the family of subsets of R×Ω whose preimage under Φ lies in F is a σ-algebra (preimages commute with complements and countable unions) containing the rectangles, which generate R⊗T (Generated Sigma-Algebra), Φ is measurable with respect to F and R⊗T. Consequently, for H as in the statement, ω↦H(W(ω),ω)=(H∘Φ)(ω) is F-measurable, since {H∘Φ>a}=Φ−1({H>a}) for every real a. Let PΦ be the image measure of P under Φ on (R×Ω,R⊗T) (claim 1 of that lemma); it satisfies PΦ(R×Ω)=1.
Step 2 (The density measure). The product measure ρ⊗PT exists on R⊗T, both factors being σ-finite. By the Tonelli theorem, for every R⊗T-measurable Ψ:R×Ω→[0,∞] the sections r↦Ψ(r,ω) are R-measurable, the map ω↦∫RΨ(r,ω)ρ(dr) is T-measurable, and
∫R×ΩΨd(ρ⊗PT)=∫Ω(∫RΨ(r,ω)ρ(dr))PT(dω)=E[∫RΨ(r,⋅)ρ(dr)],(1)
the last equality by (0). Let π be the measure with density f with respect to ρ⊗PT (claim 3 of that lemma; f is R⊗T-measurable with values in [0,∞)), so that π(S)=∫1Sfd(ρ⊗PT) for S∈R⊗T and ∫Ψdπ=∫Ψfd(ρ⊗PT) for every R⊗T-measurable Ψ≥0, the product Ψf being measurable (claim 1 of Linearity and Monotonicity of the Lebesgue Integral covers sums and constant multiples; for the product, {Ψf>a}=⋃q({Ψ>q}∩{f>a/q}) over positive rationals q when a≥0, and {Ψf>a}=R×Ω when a<0).
Step 3 (The two measures agree). For a measurable rectangle A×C with A∈R and C∈T, apply (1) to Ψ=1A×Cf, whose section at ω is 1C(ω)1A(r)f(r,ω), the constant factor 1C(ω) coming out of the inner integral by claim 1 of Linearity and Monotonicity of the Lebesgue Integral:
π(A×C)=E[1C∫R1A(r)f(r,⋅)ρ(dr)]=E[1C1A(W)]=P(C∩W−1(A))=PΦ(A×C),
the second equality being the hypothesis for C and A, and the third the integral of the simple function 1C∩W−1(A). In particular, with A=R and C=Ω, π(R×Ω)=1=PΦ(R×Ω). The measurable rectangles form a π-system (the intersection of A×C and A′×C′ is (A∩A′)×(C∩C′)) generating R⊗T, and π and PΦ are measures on R⊗T of equal finite total mass agreeing on it; by claim 1 of Uniqueness of Finite Measures on a Generating Pi-System and the Density of the Exponential Law, π=PΦ.
Step 4 (Conclusion). Let H:R×Ω→[0,∞] be R⊗T-measurable. The T-measurability of ω↦∫RH(r,ω)f(r,ω)ρ(dr) and the R-measurability of the sections are the Tonelli assertions of Step 2 applied to Ψ=Hf. Finally, by claim 2 of Image Measures, Measures with Densities, and Change of Variables (change of variables for PΦ), Step 3, claim 3 of that lemma (the density f of π), and (1) applied to Ψ=Hf,
E[H(W,⋅)]=∫ΩH∘ΦdP=∫R×ΩHdPΦ=∫R×ΩHdπ=∫R×ΩHfd(ρ⊗PT)=E[∫RH(r,⋅)f(r,⋅)ρ(dr)],
which is the asserted identity.