∀ {M : Type u_1} [inst : Monoid M] {N : Type u_2} [inst_1 : Monoid N] {φ : M →* N} (R' : Type u_11) [inst_2 : Ring R']
  [inst_3 : MulSemiringAction M R'] (S' : Type u_13) [inst_4 : Ring S'] [inst_5 : MulSemiringAction N S']
  (f : R' →ₑ+*[φ] S') (x y : R'), f (x - y) = f x - f y