∀ {B : Type u_1} [inst : TopologicalSpace B] {F₁ : Type u_2} [inst_1 : TopologicalSpace F₁] {E₁ : B → Type u_3}
  [inst_2 : TopologicalSpace (Bundle.TotalSpace F₁ E₁)] {F₂ : Type u_4} [inst_3 : TopologicalSpace F₂]
  {E₂ : B → Type u_5} [inst_4 : TopologicalSpace (Bundle.TotalSpace F₂ E₂)]
  {e₁ : Trivialization F₁ Bundle.TotalSpace.proj} {e₂ : Trivialization F₂ Bundle.TotalSpace.proj}
  [inst_5 : (x : B) → Zero (E₁ x)] [inst_6 : (x : B) → Zero (E₂ x)],
  ContinuousOn (Trivialization.Prod.invFun' e₁ e₂) ((e₁.baseSet ∩ e₂.baseSet) ×ˢ Set.univ)