∀ {𝕜 : Type u_1} [inst : NormedDivisionRing 𝕜] {E : Type u_2} [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E] {c : 𝕜}
  {s : Set E}, (c = 0 → s.Nonempty) → ∀ (x : E), egauge 𝕜 s (c • x) = ‖c‖ₑ * egauge 𝕜 s x