∀ (R : Type u_1) (n : Type u_2) [inst : CommSemiring R] [inst_1 : Fintype n] [inst_2 : DecidableEq n]
  (f : Module.Dual R (n → R)),
  (fun v => { toFun := dotProduct v, map_add' := ⋯, map_smul' := ⋯ })
      ((fun f i => f ((LinearMap.single R (fun a => R) i) 1)) f) =
    f