let GF be Field; :: thesis: for V being VectSp of
for W being Subspace of V
for A being Subset of st A is linearly-independent holds
A is linearly-independent Subset of
let V be VectSp of ; :: thesis: for W being Subspace of V
for A being Subset of st A is linearly-independent holds
A is linearly-independent Subset of
let W be Subspace of V; :: thesis: for A being Subset of st A is linearly-independent holds
A is linearly-independent Subset of
let A be Subset of ; :: thesis: ( A is linearly-independent implies A is linearly-independent Subset of )
the carrier of W c= the carrier of V by VECTSP_4:def 2;
then reconsider A' = A as Subset of by XBOOLE_1:1;
assume A1: A is linearly-independent ; :: thesis: A is linearly-independent Subset of

now

assume not A' is linearly-independent ; :: thesis: contradiction
then consider L being Linear_Combination of A' such that
A2: Sum L = 0. V and
A3: Carrier L <> {} by VECTSP_7:def 1;
Carrier L c= A' by VECTSP_6:def 7;
then consider LW being Linear_Combination of W such that
A4: Carrier LW = Carrier L and
A5: Sum LW = Sum L by Th13, XBOOLE_1:1;
reconsider LW = LW as Linear_Combination of A by A4, VECTSP_6:def 7;
Sum LW = 0. W by A2, A5, VECTSP_4:19;
hence contradiction by A1, A3, A4, VECTSP_7:def 1; :: thesis: verum

end;

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