let K be Field; :: thesis: for V being non trivial VectSp of K
for v, w being Vector of V
for a being Scalar of
for W being Linear_Compl of Lin {v} st v <> 0. V & w in W holds
(coeffFunctional v,W) . ((a * v) + w) = a
let V be non trivial VectSp of K; :: thesis: for v, w being Vector of V
for a being Scalar of
for W being Linear_Compl of Lin {v} st v <> 0. V & w in W holds
(coeffFunctional v,W) . ((a * v) + w) = a
let v, w be Vector of V; :: thesis: for a being Scalar of
for W being Linear_Compl of Lin {v} st v <> 0. V & w in W holds
(coeffFunctional v,W) . ((a * v) + w) = a
let a be Scalar of ; :: thesis: for W being Linear_Compl of Lin {v} st v <> 0. V & w in W holds
(coeffFunctional v,W) . ((a * v) + w) = a
let W be Linear_Compl of Lin {v}; :: thesis: ( v <> 0. V & w in W implies (coeffFunctional v,W) . ((a * v) + w) = a )
assume that
A1: v <> 0. V and
A2: w in W ; :: thesis: (coeffFunctional v,W) . ((a * v) + w) = a
set cf = coeffFunctional v,W;
thus (coeffFunctional v,W) . ((a * v) + w) = ((coeffFunctional v,W) . (a * v)) + ((coeffFunctional v,W) . w) by HAHNBAN1:def 11
.= ((coeffFunctional v,W) . (a * v)) + (0. K) by A1, A2, Th31
.= (coeffFunctional v,W) . (a * v) by RLVECT_1:def 7
.= a by A1, Th30 ; :: thesis: verum