let F be Field; :: thesis: for V being VectSp of F

for l being Linear_Combination of V

for A being Subset of V

for v being Element of V st not v in A holds

(l ! A) . v = 0. F

let V be VectSp of F; :: thesis: for l being Linear_Combination of V

for A being Subset of V

for v being Element of V st not v in A holds

(l ! A) . v = 0. F

let l be Linear_Combination of V; :: thesis: for A being Subset of V

for v being Element of V st not v in A holds

(l ! A) . v = 0. F

let A be Subset of V; :: thesis: for v being Element of V st not v in A holds

(l ! A) . v = 0. F

let v be Element of V; :: thesis: ( not v in A implies (l ! A) . v = 0. F )

assume not v in A ; :: thesis: (l ! A) . v = 0. F

then A1: v in V \ A by XBOOLE_0:def 5;

A2: dom (l ! A) = [#] V by FUNCT_2:92;

( dom ((V \ A) --> (0. F)) = V \ A & dom (l ! A) = (dom (l | A)) \/ (dom ((V \ A) --> (0. F))) ) by FUNCT_4:def 1;

then (l ! A) . v = ((V \ A) --> (0. F)) . v by A2, A1, FUNCT_4:def 1

.= 0. F by A1, FUNCOP_1:7 ;

hence (l ! A) . v = 0. F ; :: thesis: verum

for l being Linear_Combination of V

for A being Subset of V

for v being Element of V st not v in A holds

(l ! A) . v = 0. F

let V be VectSp of F; :: thesis: for l being Linear_Combination of V

for A being Subset of V

for v being Element of V st not v in A holds

(l ! A) . v = 0. F

let l be Linear_Combination of V; :: thesis: for A being Subset of V

for v being Element of V st not v in A holds

(l ! A) . v = 0. F

let A be Subset of V; :: thesis: for v being Element of V st not v in A holds

(l ! A) . v = 0. F

let v be Element of V; :: thesis: ( not v in A implies (l ! A) . v = 0. F )

assume not v in A ; :: thesis: (l ! A) . v = 0. F

then A1: v in V \ A by XBOOLE_0:def 5;

A2: dom (l ! A) = [#] V by FUNCT_2:92;

( dom ((V \ A) --> (0. F)) = V \ A & dom (l ! A) = (dom (l | A)) \/ (dom ((V \ A) --> (0. F))) ) by FUNCT_4:def 1;

then (l ! A) . v = ((V \ A) --> (0. F)) . v by A2, A1, FUNCT_4:def 1

.= 0. F by A1, FUNCOP_1:7 ;

hence (l ! A) . v = 0. F ; :: thesis: verum