∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [WeaklyLocallyCompactSpace X] [SigmaCompactSpace X]
  [inst_3 : TopologicalSpace Y] [TopologicalSpace.PseudoMetrizableSpace Y],
  TopologicalSpace.PseudoMetrizableSpace C(X, Y)