∀ {R : Type u_1} {M : Type u_2} {ι : Type u_6} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  [inst_3 : TopologicalSpace M] {ι' : Type u_7} {N : ι' → Type u_8} [inst_4 : (i : ι') → AddCommMonoid (N i)]
  [inst_5 : (i : ι') → TopologicalSpace (N i)] [inst_6 : (i : ι') → Module R (N i)] (f : M [⋀^ι]→L[R] ((i : ι') → N i))
  (i : ι'), ContinuousAlternatingMap.piEquiv.symm f i = (ContinuousLinearMap.proj i).compContinuousAlternatingMap f