∀ {α : Type u_1} {β : Type u_2} {ι : Type u_3} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} [inst : Countable ι]
  (κ η : ι → ProbabilityTheory.Kernel α β),
  (ProbabilityTheory.Kernel.sum fun n => κ n + η n) = ProbabilityTheory.Kernel.sum κ + ProbabilityTheory.Kernel.sum η