∀ {ι : Type u_1} [Countable ι] {a : ι → ℂ} {r : ι → ℝ} {F : ℝ → ℂ} {s : ℂ},
  0 < s.re →
    (∀ t ∈ Set.Ioi 0, HasSum (fun i => if r i = 0 then 0 else a i * ↑(Real.exp (-Real.pi * r i ^ 2 * t))) (F t)) →
      (Summable fun i => ‖a i‖ / |r i| ^ s.re) → HasSum (fun i => s.Gammaℝ * a i / ↑|r i| ^ s) (mellin F (s / 2))