∀ {X : Type u_2} {Y : Type u_1} {Z : Type u_3} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
  [inst_2 : TopologicalSpace Z] (e : OpenPartialHomeomorph X Y) (e' : OpenPartialHomeomorph Y Z),
  (e.symm.restrOpen e'.source ⋯).symm.target = (e'.restrOpen e.target ⋯).source