let K be Field; 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; 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; 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 ; 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}; ( 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
; (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 VECTSP_1:def 20
.=
((coeffFunctional (v,W)) . (a * v)) + (0. K)
by A1, A2, Th30
.=
(coeffFunctional (v,W)) . (a * v)
by RLVECT_1:def 4
.=
a
by A1, Th29
; verum