∀ {a : ℕ → ℂ},
  0 ≤ a →
    0 < a 1 →
      ∀ {f : ℂ → ℂ},
        Differentiable ℂ f →
          ∀ {x : ℝ}, LSeries.abscissaOfAbsConv a ≤ ↑x → Set.EqOn f (LSeries a) {s | x < s.re} → ∀ (y : ℝ), 0 < f ↑y