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 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 ; :: thesis: verum

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 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 ; :: thesis: verum