∀ {X : Type u_4} {X' : Type u_2} {Y : Type u_3} {Y' : Type u_1} [inst : TopologicalSpace X]
  [inst_1 : TopologicalSpace X'] [inst_2 : TopologicalSpace Y] [inst_3 : TopologicalSpace Y']
  (eX : OpenPartialHomeomorph X X') (eY : OpenPartialHomeomorph Y Y'),
  ContinuousOn (Prod.map ↑eX.symm ↑eY.symm) (eX.target ×ˢ eY.target)