∀ {ι : Type u_1} {T : Type u_4} {X : ι → Type u_5} {mX : (i : ι) → MeasurableSpace (X i)}
  [inst : (i : ι) → TopologicalSpace (X i)] [∀ (i : ι), BorelSpace (X i)] [∀ (i : ι), HasOuterApproxClosed (X i)]
  {mT : MeasurableSpace T} [inst_3 : TopologicalSpace T] [BorelSpace T] [HasOuterApproxClosed T] [Finite ι]
  {μ ν : MeasureTheory.Measure (((i : ι) → X i) × T)} [MeasureTheory.IsFiniteMeasure μ]
  [MeasureTheory.IsFiniteMeasure ν],
  (∀ (f : BoundedContinuousFunction ((i : ι) → X i) ℝ) (g : BoundedContinuousFunction T ℝ),
      ∫ (p : ((i : ι) → X i) × T), f p.1 * g p.2 ∂μ = ∫ (p : ((i : ι) → X i) × T), f p.1 * g p.2 ∂ν) →
    μ = ν