∀ {M₁ : Type u_2} {M₂ : Type u_1} {R : Type u_3} {S : Type u_4} [inst : TopologicalSpace M₂] [inst_1 : T2Space M₂]
  [inst_2 : Semiring R] [inst_3 : Semiring S] [inst_4 : AddCommMonoid M₁] [inst_5 : AddCommMonoid M₂]
  [inst_6 : Module R M₁] [inst_7 : Module S M₂] [inst_8 : ContinuousAdd M₂] {σ : R →+* S} (f : M₁ → M₂)
  (hf : f ∈ closure (Set.range DFunLike.coe)) (x y : M₁),
  (↑(addMonoidHomOfMemClosureRangeCoe f hf)).toFun (x + y) =
    (↑(addMonoidHomOfMemClosureRangeCoe f hf)).toFun x + (↑(addMonoidHomOfMemClosureRangeCoe f hf)).toFun y