English
If f and g agree on every element of s, then their images of s are equal: f''s = g''s.
Русский
Если функции f и g согласованы на каждом элементе множества s, то их образы множества s совпадают: f''s = g''s.
LaTeX
$$$ (\\forall a \\in s, f(a) = g(a)) \\Rightarrow f''s = g''s. $$$
Lean4
@[congr]
theorem image_congr {f g : α → β} {s : Set α} (h : ∀ a ∈ s, f a = g a) : f '' s = g '' s := by aesop