∀ {K : Type u_3} {L : Type u_4} [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L] {ι : Type u_5}
  {t : ι → IntermediateField K L} {p : ι → Polynomial K} {s : Finset ι},
  ∏ i ∈ s, p i ≠ 0 →
    (∀ i ∈ s, Polynomial.IsSplittingField K (↥(t i)) (p i)) →
      Polynomial.IsSplittingField K (↥(⨆ i ∈ s, t i)) (∏ i ∈ s, p i)