∀ {α : Type u} {β : Type v} {γ : Type w} [inst : TopologicalSpace α] {δ : Type u_2} [inst_1 : TopologicalSpace β]
  [inst_2 : TopologicalSpace γ] [inst_3 : TopologicalSpace δ] [inst_4 : Zero δ] (f : ZeroAtInftyContinuousMap γ δ)
  (g : CocompactMap β γ) (h : CocompactMap α β), (f.comp g).comp h = f.comp (g.comp h)