let F be Field; :: thesis: for V being VectSp of F
for X being Subset of V st X is linearly-dependent holds
ex l being Linear_Combination of X st
( Carrier l <> {} & Sum l = 0. V )
let V be VectSp of F; :: thesis: for X being Subset of V st X is linearly-dependent holds
ex l being Linear_Combination of X st
( Carrier l <> {} & Sum l = 0. V )
let X be Subset of V; :: thesis: ( X is linearly-dependent implies ex l being Linear_Combination of X st
( Carrier l <> {} & Sum l = 0. V ) )
assume X is linearly-dependent ; :: thesis: ex l being Linear_Combination of X st
( Carrier l <> {} & Sum l = 0. V )
then ex l being Linear_Combination of X st
( Sum l = 0. V & not Carrier l = {} ) by VECTSP_7:def 1;
hence ex l being Linear_Combination of X st
( Carrier l <> {} & Sum l = 0. V ) ; :: thesis: verum