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