∀ {α : Type u_1} {M : Type u_5} {N : Type u_7} {R : Type u_11} {S : Type u_12} [inst : Zero M]
  [inst_1 : SMulZeroClass R M] [inst_2 : Zero N] [inst_3 : SMulZeroClass S N] {f : M → N} {hf : f 0 = 0} (c : R) (d : S)
  (v : α →₀ M), (∀ (x : M), f (c • x) = d • f x) → Finsupp.mapRange f hf (c • v) = d • Finsupp.mapRange f hf v