let K be Ring; :: thesis: for V being LeftMod of K

for a being Vector of V

for A being Subset of V

for l being Linear_Combination of A st not a in A holds

l . a = 0. K

let V be LeftMod of K; :: thesis: for a being Vector of V

for A being Subset of V

for l being Linear_Combination of A st not a in A holds

l . a = 0. K

let a be Vector of V; :: thesis: for A being Subset of V

for l being Linear_Combination of A st not a in A holds

l . a = 0. K

let A be Subset of V; :: thesis: for l being Linear_Combination of A st not a in A holds

l . a = 0. K

let l be Linear_Combination of A; :: thesis: ( not a in A implies l . a = 0. K )

assume A1: not a in A ; :: thesis: l . a = 0. K

Carrier l c= A by VECTSP_6:def 4;

then not a in Carrier l by A1;

hence l . a = 0. K by VECTSP_6:2; :: thesis: verum

for a being Vector of V

for A being Subset of V

for l being Linear_Combination of A st not a in A holds

l . a = 0. K

let V be LeftMod of K; :: thesis: for a being Vector of V

for A being Subset of V

for l being Linear_Combination of A st not a in A holds

l . a = 0. K

let a be Vector of V; :: thesis: for A being Subset of V

for l being Linear_Combination of A st not a in A holds

l . a = 0. K

let A be Subset of V; :: thesis: for l being Linear_Combination of A st not a in A holds

l . a = 0. K

let l be Linear_Combination of A; :: thesis: ( not a in A implies l . a = 0. K )

assume A1: not a in A ; :: thesis: l . a = 0. K

Carrier l c= A by VECTSP_6:def 4;

then not a in Carrier l by A1;

hence l . a = 0. K by VECTSP_6:2; :: thesis: verum