let V be RealLinearSpace; :: thesis: for W being Subspace of V st V is finite-dimensional holds

W is finite-dimensional

let W be Subspace of V; :: thesis: ( V is finite-dimensional implies W is finite-dimensional )

set A = the Basis of W;

consider I being Basis of V such that

A1: the Basis of W c= I by Th16;

assume V is finite-dimensional ; :: thesis: W is finite-dimensional

then I is finite by Th23;

hence W is finite-dimensional by A1; :: thesis: verum

W is finite-dimensional

let W be Subspace of V; :: thesis: ( V is finite-dimensional implies W is finite-dimensional )

set A = the Basis of W;

consider I being Basis of V such that

A1: the Basis of W c= I by Th16;

assume V is finite-dimensional ; :: thesis: W is finite-dimensional

then I is finite by Th23;

hence W is finite-dimensional by A1; :: thesis: verum