∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type uE} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {s : Set E} {ι : Type u_3} [inst_3 : Fintype ι] {F' : ι → Type u_5}
  [inst_4 : (i : ι) → NormedAddCommGroup (F' i)] [inst_5 : (i : ι) → NormedSpace 𝕜 (F' i)] {Φ : E → (i : ι) → F' i}
  {P' : E → FormalMultilinearSeries 𝕜 E ((i : ι) → F' i)} {n : WithTop ℕ∞},
  HasFTaylorSeriesUpToOn n Φ P' s =
    ∀ (i : ι),
      HasFTaylorSeriesUpToOn n (fun x => Φ x i)
        (fun x m => (ContinuousLinearMap.proj i).compContinuousMultilinearMap (P' x m)) s