let V be RealLinearSpace; :: thesis: for A being Subset of V st A is linearly-independent holds

ex I being Basis of V st A c= I

let A be Subset of V; :: thesis: ( A is linearly-independent implies ex I being Basis of V st A c= I )

assume A is linearly-independent ; :: thesis: ex I being Basis of V st A c= I

then consider B being Subset of V such that

A1: A c= B and

A2: ( B is linearly-independent & Lin B = RLSStruct(# the carrier of V, the ZeroF of V, the U5 of V, the Mult of V #) ) by RLVECT_3:24;

reconsider B = B as Basis of V by A2, RLVECT_3:def 3;

take B ; :: thesis: A c= B

thus A c= B by A1; :: thesis: verum

ex I being Basis of V st A c= I

let A be Subset of V; :: thesis: ( A is linearly-independent implies ex I being Basis of V st A c= I )

assume A is linearly-independent ; :: thesis: ex I being Basis of V st A c= I

then consider B being Subset of V such that

A1: A c= B and

A2: ( B is linearly-independent & Lin B = RLSStruct(# the carrier of V, the ZeroF of V, the U5 of V, the Mult of V #) ) by RLVECT_3:24;

reconsider B = B as Basis of V by A2, RLVECT_3:def 3;

take B ; :: thesis: A c= B

thus A c= B by A1; :: thesis: verum