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