Homomorphism_Preserves_Subsemigroups

import Mathlib.Data.Set.Function
import Mathlib.Algebra.Group.Defs

theorem Homomorphism_Preserves_Subsemigroups {G H : Type _} [Group G] [Group H] (f : G → H) (hf : ∀ a b : G, f (a * b) = f a * f b) (S : Set G) (hclosed : ∀ a b : G, a ∈ S → b ∈ S → a * b ∈ S) (a b : H) (ha : a ∈ f '' S) (hb : b ∈ f '' S) : a * b ∈ f '' S := by sorry