let GF be Field; :: thesis: for V being VectSp of GF
for W being Subspace of V st V is finite-dimensional holds
W is finite-dimensional
let V be VectSp of GF; :: 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 Th13;
assume V is finite-dimensional ; :: thesis: W is finite-dimensional
then I is finite by Th20;
hence W is finite-dimensional by A1, MATRLIN:def 1; :: thesis: verum