let GF be Field; :: thesis: for V being VectSp of GF
for A, B being Subset of V st A c= B & B is linearly-independent holds
A is linearly-independent
let V be VectSp of GF; :: thesis: for A, B being Subset of V st A c= B & B is linearly-independent holds
A is linearly-independent
let A, B be Subset of V; :: thesis: ( A c= B & B is linearly-independent implies A is linearly-independent )
assume that
A1: A c= B and
A2: B is linearly-independent ; :: thesis: A is linearly-independent
let l be Linear_Combination of A; :: according to VECTSP_7:def 1 :: thesis: ( Sum l = 0. V implies Carrier l = {} )
reconsider L = l as Linear_Combination of B by A1, VECTSP_6:25;
assume Sum l = 0. V ; :: thesis: Carrier l = {}
then Carrier L = {} by A2, Def1;
hence Carrier l = {} ; :: thesis: verum