no goals
α : Type u_2
β : Type u_3
ι : Type u_1
mα : MeasurableSpace α
mβ : MeasurableSpace β
I : Finset ι
κ : ι → { x // x ∈ kernel α β }
a : α
s : Set β
⊢ ↑↑(↑(∑ i in I, κ i) a) s = ∑ i in I, ↑↑(↑(κ i) a) s
rw [finset_sum_apply, Measure.finset_sum_apply]