{R : Type u_1} →
  {B : Type u_2} →
    {F : Type u_3} →
      {E : B → Type u_4} →
        [inst : NontriviallyNormedField R] →
          [inst_1 : (x : B) → AddCommMonoid (E x)] →
            [inst_2 : (x : B) → Module R (E x)] →
              [inst_3 : NormedAddCommGroup F] →
                [inst_4 : NormedSpace R F] →
                  [inst_5 : TopologicalSpace B] →
                    [inst_6 : TopologicalSpace (Bundle.TotalSpace F E)] →
                      [inst_7 : (x : B) → TopologicalSpace (E x)] →
                        [inst_8 : FiberBundle F E] →
                          {motive : VectorBundle R F E → Sort u} →
                            ((trivialization_linear' :
                                  ∀ (e : Trivialization F Bundle.TotalSpace.proj) [MemTrivializationAtlas e],
                                    Trivialization.IsLinear R e) →
                                (continuousOn_coordChange' :
                                    ∀ (e e' : Trivialization F Bundle.TotalSpace.proj)
                                      [inst_9 : MemTrivializationAtlas e] [inst_10 : MemTrivializationAtlas e'],
                                      ContinuousOn (fun b => ↑(Trivialization.coordChangeL R e e' b))
                                        (e.baseSet ∩ e'.baseSet)) →
                                  motive ⋯) →
                              (t : VectorBundle R F E) → motive t