Morphism_Property_Preserves_Closure

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

theorem Morphism_Property_Preserves_Closure {G H : Type _} [Mul G] [Mul H] (f : G → H) (hf : ∀ a b : G, f (a * b) = f a * f b) (S : Set G) (hS : ∀ a b : G, a ∈ S → b ∈ S → a * b ∈ S) : ∀ a b : H, a ∈ f '' S → b ∈ f '' S → ∃ c ∈ f '' S, c = a * b := by sorry