∀ {V₁ : Type u_2} {V₂ : Type u_3} {V₃ : Type u_4} [inst : SeminormedAddCommGroup V₁]
  [inst_1 : SeminormedAddCommGroup V₂] [inst_2 : SeminormedAddCommGroup V₃] (g : NormedAddGroupHom V₂ V₃)
  (f : NormedAddGroupHom V₁ V₂) (a : V₁), (g.comp f) a = g (f a)