∀ {M N O : Type u} [inst : SeminormedAddCommGroup M] [inst_1 : SeminormedAddCommGroup N]
  [inst_2 : SeminormedAddCommGroup O] (f : NormedAddGroupHom M N) (g : NormedAddGroupHom N O) (hf : f.NormNoninc)
  (hg : g.NormNoninc) (hgf : (g.comp f).NormNoninc),
  SemiNormedGrp₁.mkHom (g.comp f) hgf =
    CategoryTheory.CategoryStruct.comp (SemiNormedGrp₁.mkHom f hf) (SemiNormedGrp₁.mkHom g hg)