∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_5} {ι : Type u_4} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : SeminormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] [inst_3 : SeminormedAddCommGroup F]
  [inst_4 : NormedSpace 𝕜 F] [inst_5 : SeminormedAddCommGroup G] [inst_6 : NormedSpace 𝕜 G] [inst_7 : Fintype ι]
  [inst_8 : DecidableEq ι] (f : F [⋀^ι]→L[𝕜] G) (g x : E →L[𝕜] F) (v : ι → E) (i j : ι),
  v i = v j →
    i ≠ j →
      (((f.fderivCompContinuousLinearMap fun x => g).comp
              (ContinuousLinearMap.pi fun x => ContinuousLinearMap.id 𝕜 (E →L[𝕜] F)))
            x)
          v =
        0