∀ {𝕜 : Type u_1} {B : Type u_2} {F : Type u_3} [inst : TopologicalSpace B] [inst_1 : NontriviallyNormedField 𝕜]
  [inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace 𝕜 F] {U U_1 : Set B} (e_U : U = U_1) (φ φ_1 : B → F ≃L[𝕜] F)
  (e_φ : φ = φ_1) (hU : IsOpen U) (hφ : ContinuousOn (fun x => ↑(φ x)) U) (h2φ : ContinuousOn (fun x => ↑(φ x).symm) U),
  FiberwiseLinear.openPartialHomeomorph φ hU hφ h2φ = FiberwiseLinear.openPartialHomeomorph φ_1 ⋯ ⋯ ⋯