let GF be Field; :: thesis: for V being VectSp of GF
for W being Subspace of V
for A being Subset of V st A is linearly-independent & A c= the carrier of W holds
A is linearly-independent Subset of W
let V be VectSp of GF; :: thesis: for W being Subspace of V
for A being Subset of V st A is linearly-independent & A c= the carrier of W holds
A is linearly-independent Subset of W
let W be Subspace of V; :: thesis: for A being Subset of V st A is linearly-independent & A c= the carrier of W holds
A is linearly-independent Subset of W
let A be Subset of V; :: thesis: ( A is linearly-independent & A c= the carrier of W implies A is linearly-independent Subset of W )
assume that
A1: A is linearly-independent and
A2: A c= the carrier of W ; :: thesis: A is linearly-independent Subset of W
reconsider A9 = A as Subset of W by A2;

now :: thesis: not A9 is linearly-dependent

assume A9 is linearly-dependent ; :: thesis: contradiction
then consider K being Linear_Combination of A9 such that
A3: Sum K = 0. W and
A4: Carrier K <> {} by VECTSP_7:def 1;
consider L being Linear_Combination of V such that
A5: Carrier L = Carrier K and
A6: Sum L = Sum K by Th8;
reconsider L = L as Linear_Combination of A by A5, VECTSP_6:def 4;
Sum L = 0. V by A3, A6, VECTSP_4:11;
hence contradiction by A1, A4, A5, VECTSP_7:def 1; :: thesis: verum

end;

hence A is linearly-independent Subset of W ; :: thesis: verum