∀ {B : Type u_3} {F : Type u_2} {Z : Type u_1} [inst : TopologicalSpace B] [inst_1 : TopologicalSpace F] {proj : Z → B}
  [inst_2 : TopologicalSpace Z] (e e' : Bundle.Trivialization F proj) (s : Set B)
  (Hs : e.baseSet ∩ frontier s = e'.baseSet ∩ frontier s)
  (Heq : Set.EqOn (↑e) (↑e') (proj ⁻¹' (e.baseSet ∩ frontier s))),
  (e.piecewise e'.toOpenPartialHomeomorph (proj ⁻¹' s) (s ×ˢ Set.univ) ⋯ ⋯ ⋯ ⋯).source =
    proj ⁻¹' s.ite e.baseSet e'.baseSet