∀ {α : Type u_1} {β : Type u_3} {γ : Type u_5} {δ : Type u_7} {δ' : Type u_8} {ε : Type u_9} {s : Set α} {t : Set β}
  {u : Set γ} {f : α → δ → ε} {g : β → γ → δ} {f' : α → γ → δ'} {g' : β → δ' → ε},
  (∀ (a : α) (b : β) (c : γ), f a (g b c) = g' b (f' a c)) →
    Set.image2 f s (Set.image2 g t u) = Set.image2 g' t (Set.image2 f' s u)