∀ {𝕜 : Type u_1} {B : Type u_2} [inst : NontriviallyNormedField 𝕜] [inst_1 : TopologicalSpace B] {F₁ : Type u_3}
  [inst_2 : NormedAddCommGroup F₁] [inst_3 : NormedSpace 𝕜 F₁] {E₁ : B → Type u_4}
  [inst_4 : TopologicalSpace (Bundle.TotalSpace F₁ E₁)] {F₂ : Type u_5} [inst_5 : NormedAddCommGroup F₂]
  [inst_6 : NormedSpace 𝕜 F₂] {E₂ : B → Type u_6} [inst_7 : TopologicalSpace (Bundle.TotalSpace F₂ E₂)]
  [inst_8 : (x : B) → AddCommMonoid (E₁ x)] [inst_9 : (x : B) → Module 𝕜 (E₁ x)]
  [inst_10 : (x : B) → AddCommMonoid (E₂ x)] [inst_11 : (x : B) → Module 𝕜 (E₂ x)]
  [inst_12 : (x : B) → TopologicalSpace (E₁ x)] [inst_13 : (x : B) → TopologicalSpace (E₂ x)]
  [inst_14 : FiberBundle F₁ E₁] [inst_15 : FiberBundle F₂ E₂] {e₁ : Bundle.Trivialization F₁ Bundle.TotalSpace.proj}
  {e₂ : Bundle.Trivialization F₂ Bundle.TotalSpace.proj} [inst_16 : Bundle.Trivialization.IsLinear 𝕜 e₁]
  [inst_17 : Bundle.Trivialization.IsLinear 𝕜 e₂] {x : B} (hx : x ∈ (e₁.prod e₂).baseSet),
  Bundle.Trivialization.continuousLinearEquivAt 𝕜 (e₁.prod e₂) x hx =
    (Bundle.Trivialization.continuousLinearEquivAt 𝕜 e₁ x ⋯).prodCongr
      (Bundle.Trivialization.continuousLinearEquivAt 𝕜 e₂ x ⋯)