∀ {E : Type u} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {n : ℕ} (I : BoxIntegral.Box (Fin (n + 1)))
  (f : (Fin (n + 1) → ℝ) → Fin (n + 1) → E) (f' : (Fin (n + 1) → ℝ) → (Fin (n + 1) → ℝ) →L[ℝ] Fin (n + 1) → E)
  (s : Set (Fin (n + 1) → ℝ)),
  s.Countable →
    ContinuousOn f (BoxIntegral.Box.Icc I) →
      (∀ x ∈ BoxIntegral.Box.Ioo I \ s, HasFDerivAt f (f' x) x) →
        MeasureTheory.IntegrableOn (fun x => ∑ i, (f' x) (Pi.single i 1) i) (BoxIntegral.Box.Icc I)
            MeasureTheory.volume →
          ∫ (x : Fin (n + 1) → ℝ) in BoxIntegral.Box.Icc I, ∑ i, (f' x) (Pi.single i 1) i =
            ∑ i,
              ((∫ (x : Fin n → ℝ) in BoxIntegral.Box.Icc (I.face i), f (i.insertNth (I.upper i) x) i) -
                ∫ (x : Fin n → ℝ) in BoxIntegral.Box.Icc (I.face i), f (i.insertNth (I.lower i) x) i)