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 )
the carrier of W c= the carrier of V by RUSUB_1:def 1;
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
assume 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 <> {} ;
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 Th20, XBOOLE_1:1;
reconsider LW = LW as Linear_Combination of A by A4, RLVECT_2:def 6;
Sum LW = 0. W by A2, A5, RUSUB_1:4;
hence contradiction by A1, A3, A4; :: thesis: verum
end;
hence A is linearly-independent Subset of V ; :: thesis: verum