∀ {B : Type u_1} {F : Type u_2} {Z : Type u_4} [inst : TopologicalSpace B] [inst_1 : TopologicalSpace F] {proj : Z → B}
  [inst_2 : TopologicalSpace Z] (e₁ e₂ : Trivialization F proj) {b : B} (h₁ : b ∈ e₁.baseSet) (h₂ : b ∈ e₂.baseSet),
  ⇑(e₁.coordChangeHomeomorph e₂ h₁ h₂) = e₁.coordChange e₂ b