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, STRUCT_0:def 5;
w in the carrier of W by A2, STRUCT_0:def 5;
hence (coeffFunctional v,W) . w = ((coeffFunctional v,W) | the carrier of W) . w by FUNCT_1:72
.= (0Functional W) . s by A1, Def8
.= 0. K by HAHNBAN1:22 ;
:: thesis: verum