∀ {V₁ : Type u_2} {V₂ : Type u_3} [inst : SeminormedAddCommGroup V₁] [inst_1 : SeminormedAddCommGroup V₂] {R : Type u_5}
  [inst_2 : MonoidWithZero R] [inst_3 : DistribMulAction R V₂] [inst_4 : PseudoMetricSpace R]
  [inst_5 : IsBoundedSMul R V₂] (r : R) (f : NormedAddGroupHom V₁ V₂) (v : V₁), (r • f) v = r • f v