∀ {R : Type u_1} {E : Type u_5} {E₂ : Type u_6} [inst : Semiring R] [inst_1 : SeminormedAddCommGroup E]
  [inst_2 : SeminormedAddCommGroup E₂] [inst_3 : Module R E] [inst_4 : Module R E₂] {e : E ≃ₗᵢ[R] E₂} (c : R) (x : E),
  e (c • x) = c • e x