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