let W be RealLinearSpace; :: thesis: ( W is finite-dimensional iff RLSp2RVSp W is finite-dimensional )

hereby :: thesis: ( RLSp2RVSp W is finite-dimensional implies W is finite-dimensional )

assume W is finite-dimensional ; :: thesis: RLSp2RVSp W is finite-dimensional
then ex A being finite Subset of W st A is Basis of W by RLVECT_5:def 1;
hence RLSp2RVSp W is finite-dimensional by Th80; :: thesis: verum

end;

thus ( RLSp2RVSp W is finite-dimensional implies W is finite-dimensional ) by Th80, RLVECT_5:def 1; :: thesis: verum