∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : CommMonoid α] [inst_1 : TopologicalSpace α]
  {L : SummationFilter β} [ContinuousMul α] {f : γ → β → α} {a : γ → α} {s : Finset γ},
  (∀ i ∈ s, HasProd (f i) (a i) L) → HasProd (fun b => ∏ i ∈ s, f i b) (∏ i ∈ s, a i) L