∀ {E : Type u_1} [inst : NormedAddCommGroup E] {f : ℝ → E} {T : ℝ} [inst_1 : NormedSpace ℝ E],
  Function.Periodic f T →
    ∀ (n : ℤ) (t : ℝ),
      (∀ (t₁ t₂ : ℝ), IntervalIntegrable f MeasureTheory.volume t₁ t₂) →
        ∫ (x : ℝ) in t..t + n • T, f x = n • ∫ (x : ℝ) in t..t + T, f x