∀ {K : Type u_1} {L : Type u_2} [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L] (S : IntermediateField K L)
  {ι : Type u_4} {t : Finset ι} {f : ι → L}, (∀ c ∈ t, f c ∈ S) → ∑ i ∈ t, f i ∈ S