∀ {M : Type u_1} {N : Type u_2} {F : Type u_3} {α : Type u_4} {β : Type u_5} {σ : M → N} [inst : SMul M α]
  [inst_1 : SMul N β] [inst_2 : FunLike F α β] [MulActionSemiHomClass F σ α β] (f : F) (c : M) (s : Set α),
  σ c • ⇑f '' s = ⇑f '' (c • s)