let V be RealLinearSpace; :: thesis: for W being Subspace of V

for A being Basis of W ex B being Basis of V st A c= B

let W be Subspace of V; :: thesis: for A being Basis of W ex B being Basis of V st A c= B

let A be Basis of W; :: thesis: ex B being Basis of V st A c= B

A is linearly-independent by RLVECT_3:def 3;

then A is linearly-independent Subset of V by Th14;

then consider I being Basis of V such that

A1: A c= I by Th2;

take I ; :: thesis: A c= I

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

for A being Basis of W ex B being Basis of V st A c= B

let W be Subspace of V; :: thesis: for A being Basis of W ex B being Basis of V st A c= B

let A be Basis of W; :: thesis: ex B being Basis of V st A c= B

A is linearly-independent by RLVECT_3:def 3;

then A is linearly-independent Subset of V by Th14;

then consider I being Basis of V such that

A1: A c= I by Th2;

take I ; :: thesis: A c= I

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