∀ {V₁ : Type u_3} [inst : SeminormedAddCommGroup V₁] {W₁ : Type u_6} [inst_1 : SeminormedAddCommGroup W₁]
  {f₁ g₁ : NormedAddGroupHom V₁ W₁},
  NormedAddGroupHom.Equalizer.map (NormedAddGroupHom.id V₁) (NormedAddGroupHom.id W₁) ⋯ ⋯ =
    NormedAddGroupHom.id ↥(f₁.equalizer g₁)