let V be RealLinearSpace; :: 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 )

the carrier of W c= the carrier of V by RLSUB_1:def 2;

then reconsider A9 = A as Subset of V by XBOOLE_1:1;

assume A1: A is linearly-independent ; :: thesis: A is linearly-independent Subset 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 )

the carrier of W c= the carrier of V by RLSUB_1:def 2;

then reconsider A9 = A as Subset of V by XBOOLE_1:1;

assume A1: A is linearly-independent ; :: thesis: A is linearly-independent Subset of V

now :: thesis: not A9 is linearly-dependent

hence
A is linearly-independent Subset of V
; :: thesis: verumassume
A9 is linearly-dependent
; :: thesis: contradiction

then consider L being Linear_Combination of A9 such that

A2: Sum L = 0. V and

A3: Carrier L <> {} by RLVECT_3:def 1;

Carrier L c= A by RLVECT_2:def 6;

then consider LW being Linear_Combination of W such that

A4: Carrier LW = Carrier L and

A5: Sum LW = Sum L by Th12, XBOOLE_1:1;

reconsider LW = LW as Linear_Combination of A by A4, RLVECT_2:def 6;

Sum LW = 0. W by A2, A5, RLSUB_1:11;

hence contradiction by A1, A3, A4, RLVECT_3:def 1; :: thesis: verum

end;then consider L being Linear_Combination of A9 such that

A2: Sum L = 0. V and

A3: Carrier L <> {} by RLVECT_3:def 1;

Carrier L c= A by RLVECT_2:def 6;

then consider LW being Linear_Combination of W such that

A4: Carrier LW = Carrier L and

A5: Sum LW = Sum L by Th12, XBOOLE_1:1;

reconsider LW = LW as Linear_Combination of A by A4, RLVECT_2:def 6;

Sum LW = 0. W by A2, A5, RLSUB_1:11;

hence contradiction by A1, A3, A4, RLVECT_3:def 1; :: thesis: verum