∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [TopologicalSpace.IsCompletelyPseudoMetrizableSpace X]
  [inst_2 : TopologicalSpace Y] [TopologicalSpace.IsCompletelyPseudoMetrizableSpace Y],
  TopologicalSpace.IsCompletelyPseudoMetrizableSpace (X ⊕ Y)