∀ {α : Type u_4} {α' : Type u_6} {β : Type u_5} {β' : Type u_7} {γ : Type u_3} {δ : Type u_2} {ε : Type u_1} {s : Set α}
  {t : Set β} {u : Set γ} {f : δ → γ → ε} {g : α → β → δ} {f₁ : α → γ → α'} {f₂ : β → γ → β'} {g' : α' → β' → ε},
  (∀ (a : α) (b : β) (c : γ), f (g a b) c = g' (f₁ a c) (f₂ b c)) →
    Set.image2 f (Set.image2 g s t) u ⊆ Set.image2 g' (Set.image2 f₁ s u) (Set.image2 f₂ t u)