theorem Th30: :: VECTSP10:30

for K being Field
for V being non trivial VectSp of K
for v, w being Vector of V
for W being Linear_Compl of Lin {v} st v <> 0. V & w in W holds
(coeffFunctional (v,W)) . w = 0. K