{M : Type u_4} →
  {N : Type u_5} →
    [inst : AddMonoid M] →
      [inst_1 : AddMonoid N] →
        {s : Set M} →
          (f : M → N) → AddSubmonoid.closure s = ⊤ → f 0 = 0 → (∀ (x y : M), y ∈ s → f (x + y) = f x + f y) → M →+ N