let W be RealLinearSpace; :: thesis: ( W is finite-dimensional implies ( RLSp2RVSp W is finite-dimensional & dim (RLSp2RVSp W) = dim W ) )
assume A1: W is finite-dimensional ; :: thesis: ( RLSp2RVSp W is finite-dimensional & dim (RLSp2RVSp W) = dim W )
then consider A being finite Subset of W such that
A2: A is Basis of W by RLVECT_5:def 1;
reconsider B = A as finite Subset of (RLSp2RVSp W) ;
A3: B is Basis of (RLSp2RVSp W) by A2, Th80;
thus RLSp2RVSp W is finite-dimensional by A2, Th80; :: thesis: dim (RLSp2RVSp W) = dim W
hence dim (RLSp2RVSp W) = card B by A3, VECTSP_9:def 1
.= dim W by A1, A2, RLVECT_5:def 2 ;
:: thesis: verum