∀ {X : Type u_1} {mX : MeasurableSpace X} {μ : MeasureTheory.Measure X} {q : ENNReal} [inst : Fact (1 ≤ q)]
  {ι : Type u_2} [inst_1 : Fintype ι] {E : ι → Type u_3} [inst_2 : (i : ι) → NormedAddCommGroup (E i)]
  {f : X → PiLp q E} [inst_3 : (i : ι) → NormedSpace ℝ (E i)] [∀ (i : ι), CompleteSpace (E i)],
  (∀ (i : ι), MeasureTheory.Integrable (fun x => (f x).ofLp i) μ) →
    ∀ (i : ι), (∫ (x : X), f x ∂μ).ofLp i = ∫ (x : X), (f x).ofLp i ∂μ