∀ {ι : Type u} {E : Type v} {F : Type w} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E]
  [inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace ℝ F] {I : BoxIntegral.Box ι} [inst_4 : Fintype ι]
  {f : (ι → ℝ) → E} {vol : BoxIntegral.BoxAdditiveMap ι (E →L[ℝ] F) ⊤} (B : BoxIntegral.BoxAdditiveMap ι ℝ ↑I),
  (∀ (J : BoxIntegral.Box ι), 0 ≤ B J) →
    ∀ (g : BoxIntegral.BoxAdditiveMap ι F ↑I),
      (∀ (x : NNReal),
          ∀ x ∈ BoxIntegral.Box.Icc I,
            ∀ ε > 0,
              ∃ δ > 0, ∀ J ≤ I, BoxIntegral.Box.Icc J ⊆ Metric.closedBall x δ → dist ((vol J) (f x)) (g J) ≤ ε * B J) →
        BoxIntegral.HasIntegral I BoxIntegral.IntegrationParams.McShane f vol (g I)