no goals
α : Type u_1
β : Type u_2
ι : Type ?u.382317
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ✝ κ : { x // x ∈ kernel α β }
h : IsSFiniteKernel κ
a : α
⊢ (Measure.sum fun n => ↑(seq κ n) a) = ↑κ a
rw [← kernel.sum_apply, kernel_sum_seq κ]