∀ {γ : Type w} {ι₁ : Type u_3} {ι₂ : Type u_4} {β₁ : ι₁ → Type u_1} {β₂ : ι₂ → Type u_2} [inst : DecidableEq ι₁]
  [inst_1 : DecidableEq ι₂] [inst_2 : (i : ι₁) → Zero (β₁ i)] [inst_3 : (i : ι₂) → Zero (β₂ i)]
  [inst_4 : (i : ι₁) → (x : β₁ i) → Decidable (x ≠ 0)] [inst_5 : (i : ι₂) → (x : β₂ i) → Decidable (x ≠ 0)]
  [inst_6 : CommMonoid γ] (f₁ : Π₀ (i : ι₁), β₁ i) (f₂ : Π₀ (i : ι₂), β₂ i) (h : (i : ι₁) → β₁ i → (i : ι₂) → β₂ i → γ),
  (f₁.prod fun i₁ x₁ => f₂.prod fun i₂ x₂ => h i₁ x₁ i₂ x₂) = f₂.prod fun i₂ x₂ => f₁.prod fun i₁ x₁ => h i₁ x₁ i₂ x₂