∀ {β : Type u_2} {γ : Type u_3} (α : Type u_1) [inst : TopologicalSpace α] [inst_1 : SeminormedRing β]
  [inst_2 : SeminormedRing γ] (g : β →+* γ) {C : NNReal} (hg : LipschitzWith C ⇑g)
  (x y : BoundedContinuousFunction α β),
  (↑(AddMonoidHom.compLeftContinuousBounded α g.toAddMonoidHom hg)).toFun (x + y) =
    (↑(AddMonoidHom.compLeftContinuousBounded α g.toAddMonoidHom hg)).toFun x +
      (↑(AddMonoidHom.compLeftContinuousBounded α g.toAddMonoidHom hg)).toFun y