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;

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

hence
A is linearly-independent Subset of W
; :: thesis: verumassume
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;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