∀ {I : Type u_1} {f : I → Type u_2} {γ : Type u_3} [inst : (i : I) → Mul (f i)] [inst_1 : Mul γ]
  (g : (i : I) → γ →ₙ* f i) (x y : γ), (fun i => (g i) (x * y)) = (fun i => (g i) x) * fun i => (g i) y