∀ {α : Type u} {β : Type v} {γ : Type w} [inst : Mul α] [inst_1 : Mul β] [inst_2 : Mul γ] (f : α →ₙ* β) (g : β →ₙ* γ)
  (x : WithOne α), (WithOne.mapMulHom g) ((WithOne.mapMulHom f) x) = (WithOne.mapMulHom (g.comp f)) x