reconsider B = RN_Base n as Subset of by FINSEQ_2:111;
B is Basis of RealVectSpace (Seg n) by Th48;
hence RealVectSpace (Seg n) is finite-dimensional by RLVECT_5:def 1; :: thesis: verum