no goals
α : Type u_2
β : Type ?u.116671
ι✝ : Type ?u.116674
M : Type u_3
N : Type ?u.116680
inst✝ : CommMonoid M
ι : Type u_1
I : Finset ι
s : ι → Set α
f : α → M
h : ∀ (i : ι), i ∈ I → ∀ (j : ι), j ∈ I → i ≠ j → Disjoint (s i) (s j)
x : α
⊢ mulIndicator (⋃ (i : ι) (_ : i ∈ I), s i) f x = ∏ i in I, mulIndicator (s i) f x
rw [Set.mulIndicator_finset_biUnion I s h]