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

now

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

end;

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