∀ {ι : Type u_1} {κ : Type u_3} {M : Type u_2} [inst : CommMonoid M] {s : Finset ι} {t : Finset κ} {f : ι → M}
  {g : κ → M} (i : (a : ι) → a ∈ s → f a ≠ 1 → κ),
  (∀ (a : ι) (h₁ : a ∈ s) (h₂ : f a ≠ 1), i a h₁ h₂ ∈ t) →
    (∀ (a : ι) (h₁ : a ∈ s) (h₂ : f a ≠ 1), f a = g (i a h₁ h₂)) →
      ∀ (a : ι) (ha : a ∈ {x ∈ s | ¬f x = 1}), i a ⋯ ⋯ ∈ {x ∈ t | ¬g x = 1}