∀ (R₁ : Type u_3) [inst : CommRing R₁] {K : Type u_4} [inst_1 : Field K] [inst_2 : Algebra R₁ K]
  [inst_3 : IsFractionRing R₁ K] {ι : Type u_5} (s s_1 : Finset ι),
  s = s_1 → ∀ (f f_1 : ι → K), f = f_1 → FractionalIdeal.spanFinset R₁ s f = FractionalIdeal.spanFinset R₁ s_1 f_1