∀ {V₁ : Type u_3} {V₂ : Type u_4} {V₃ : Type u_5} [inst : SeminormedAddCommGroup V₁]
  [inst_1 : SeminormedAddCommGroup V₂] [inst_2 : SeminormedAddCommGroup V₃] (f : NormedAddGroupHom V₁ V₂)
  (g : NormedAddGroupHom V₂ V₃), (g.comp f).range = AddSubgroup.map g.toAddMonoidHom f.range