{𝕜 : Type u_1} →
  {E : Type u_2} →
    {F : Type u_3} →
      [inst : NontriviallyNormedField 𝕜] →
        [inst_1 : NormedAddCommGroup E] →
          [inst_2 : NormedSpace 𝕜 E] →
            [inst_3 : NormedAddCommGroup F] →
              [inst_4 : NormedSpace 𝕜 F] →
                {f : E → F} →
                  {p : FormalMultilinearSeries 𝕜 E F} →
                    {x : E} →
                      {r : ENNReal} →
                        {motive : HasFPowerSeriesOnBall f p x r → Sort u} →
                          ((r_le : r ≤ p.radius) →
                              (r_pos : 0 < r) →
                                (hasSum :
                                    ∀ {y : E}, y ∈ Metric.eball 0 r → HasSum (fun n => (p n) fun x => y) (f (x + y))) →
                                  motive ⋯) →
                            (t : HasFPowerSeriesOnBall f p x r) → motive t