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