∀ {ι : Type u_1} {η : ι → Type u_2} {N : Type u_3} [inst : Zero N] (f : Π₀ (i : ι), η i →₀ N),
  (fun f => { toFun := f.split, support' := Trunc.mk ⟨f.splitSupport.val, ⋯⟩ })
      ((fun f => Finsupp.onFinset (f.support.sigma fun j => (f j).support) (fun ji => (f ji.fst) ji.snd) ⋯) f) =
    f