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 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 RLVECT_3:def 1;
consider L being Linear_Combination of V such that
A5: Carrier L = Carrier K and
A6: Sum L = Sum K by Th11;
reconsider L = L as Linear_Combination of A by A5, RLVECT_2:def 6;
Sum L = 0. V by A3, A6, RLSUB_1:11;
hence contradiction by A1, A4, A5, RLVECT_3:def 1; :: thesis: verum
end;
hence A is linearly-independent Subset of W ; :: thesis: verum