∀ {R : Type u_1} {E : Type u_3} [inst : AddGroup E] [inst_1 : SMul R ℝ] [inst_2 : SMul R NNReal]
  [inst_3 : IsScalarTower R NNReal ℝ] (r : R) (p : NonarchAddGroupSeminorm E) (x : E), (r • p) x = r • p x