let K be Field; :: thesis: 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
let V be non trivial VectSp of K; :: thesis: 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
let v, w be Vector of V; :: thesis: for W being Linear_Compl of Lin {v} st v <> 0. V & w in W holds
(coeffFunctional (v,W)) . w = 0. K
let W be Linear_Compl of Lin {v}; :: thesis: ( v <> 0. V & w in W implies (coeffFunctional (v,W)) . w = 0. K )
assume that
A1: v <> 0. V and
A2: w in W ; :: thesis: (coeffFunctional (v,W)) . w = 0. K
set cf = coeffFunctional (v,W);
set cw = the carrier of W;
reconsider s = w as Vector of W by A2;
w in the carrier of W by A2;
hence (coeffFunctional (v,W)) . w = ((coeffFunctional (v,W)) | the carrier of W) . w by FUNCT_1:49
.= (0Functional W) . s by A1, Def8
.= 0. K by HAHNBAN1:14 ;
:: thesis: verum