theorem ProbabilityTheory.IdentDistrib.prod {Ω : Type u_1} {Ω' : Type u_2} {mΩ : MeasurableSpace Ω} {mΩ' : MeasurableSpace Ω'} {μ : MeasureTheory.Measure Ω} {ν : MeasureTheory.Measure Ω'} {X Y : Ω → ℝ} {Z W : Ω' → ℝ} [MeasureTheory.IsFiniteMeasure μ] [MeasureTheory.IsFiniteMeasure ν] (hXZ : IdentDistrib X Z μ ν) (hYW : IdentDistrib Y W μ ν) (hXY : IndepFun X Y μ) (hZW : IndepFun Z W ν) : IdentDistrib (fun (ω : Ω) => (X ω, Y ω)) (fun (ω' : Ω') => (Z ω', W ω')) μ ν