∀ {α : Type u_1} {β : Type u_3} {β' : Type u_4} {γ : Type u_5} {δ : Type u_7} [inst : DecidableEq β']
  [inst_1 : DecidableEq γ] {f : α → β → γ} {s : Finset α} {t : Finset β} [inst_2 : DecidableEq δ] {g : γ → δ}
  {f' : β' → α → δ} {g' : β → β'},
  (∀ (a : α) (b : β), g (f a b) = f' (g' b) a) →
    Finset.image g (Finset.image₂ f s t) = Finset.image₂ f' (Finset.image g' t) s