let V be RealLinearSpace; :: 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 A' = A as Subset of W by A2;

now

assume not A' is linearly-independent ; :: thesis: contradiction
then consider K being Linear_Combination of A' such that
A3: ( Sum K = 0. W & Carrier K <> {} ) by RLVECT_3:def 1;
consider L being Linear_Combination of V such that
A4: ( Carrier L = Carrier K & Sum L = Sum K ) by Th12;
reconsider L = L as Linear_Combination of A by A4, RLVECT_2:def 8;
( Sum L = 0. V & Carrier L <> {} ) by A3, A4, RLSUB_1:19;
hence contradiction by A1, RLVECT_3:def 1; :: thesis: verum

end;

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