:: deftheorem Def8 defines coeffFunctional VECTSP10:def 8 :
for K being Field
for V being non trivial VectSp of K
for v being Vector of V
for W being Linear_Compl of Lin {v} st v <> 0. V holds
for b₅ being V8() non trivial linear-Functional of V holds
( b₅ = coeffFunctional (v,W) iff ( b₅ . v = 1_ K & b₅ | the carrier of W = 0Functional W ) );