∀ (R : Type u_4) {ι : Type u_1} (M₂ : Type u_2) (M₃ : Type u_3) [inst : Semiring R] [inst_1 : AddCommMonoid M₂]
  [inst_2 : AddCommMonoid M₃] [inst_3 : Module R M₂] [inst_4 : Module R M₃] [inst_5 : Subsingleton ι] (i : ι)
  (f : MultilinearMap R (fun x => M₂) M₃),
  (fun f => { toFun := fun x => f (x i), map_update_add' := ⋯, map_update_smul' := ⋯ })
      ((fun f => { toFun := fun x => f fun x_1 => x, map_add' := ⋯, map_smul' := ⋯ }) f) =
    f