∀ {𝕜 : Type u_1} {E : Type u_2} [inst : NormedField 𝕜] [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E] (f : E → ℝ),
  f 0 = 0 → (∀ (r : 𝕜) (x : E), f (r • x) ≤ ‖r‖ * f x) → ∀ (r : 𝕜) (x : E), f (r • x) = ‖r‖ * f x