let V be RealUnitarySpace; :: 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 RUSUB_1:def 1;
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 RLVECT_3:def 1;
Carrier L c= A by RLVECT_2:def 8;
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 Th20;
reconsider LW = LW as Linear_Combination of A by A3, RLVECT_2:def 8;
( Sum LW = 0. W & Carrier LW <> {} ) by A2, A3, RUSUB_1:4;
hence contradiction by A1, RLVECT_3:def 1; :: thesis: verum

end;

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