let K be Field; :: thesis: for V being non trivial VectSp of K
for v being Vector of V
for a being Scalar of
for W being Linear_Compl of Lin {v} st v <> 0. V holds
(coeffFunctional (v,W)) . (a * v) = a
let V be non trivial VectSp of K; :: thesis: for v being Vector of V
for a being Scalar of
for W being Linear_Compl of Lin {v} st v <> 0. V holds
(coeffFunctional (v,W)) . (a * v) = a
let v be Vector of V; :: thesis: for a being Scalar of
for W being Linear_Compl of Lin {v} st v <> 0. V holds
(coeffFunctional (v,W)) . (a * v) = a
let a be Scalar of ; :: thesis: for W being Linear_Compl of Lin {v} st v <> 0. V holds
(coeffFunctional (v,W)) . (a * v) = a
let W be Linear_Compl of Lin {v}; :: thesis: ( v <> 0. V implies (coeffFunctional (v,W)) . (a * v) = a )
assume A1: v <> 0. V ; :: thesis: (coeffFunctional (v,W)) . (a * v) = a
set cf = coeffFunctional (v,W);
thus (coeffFunctional (v,W)) . (a * v) = a * ((coeffFunctional (v,W)) . v) by HAHNBAN1:def 8
.= a * (1_ K) by A1, Def8
.= a ; :: thesis: verum