∀ {X : Type u_2} {Y : Type u_1} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
  (e e' : OpenPartialHomeomorph X Y) (s : Set X) (t : Set Y),
  e.IsImage s t →
    e'.IsImage s t →
      e.source ∩ frontier s = e'.source ∩ frontier s →
        Set.EqOn (↑e) (↑e') (e.source ∩ frontier s) → IsOpen (t.ite e.target e'.target)