reconsider B = RN_Base n as Subset of (REAL-L n) ;
B is Basis of REAL-L n by Th54;
hence REAL-L n is finite-dimensional by RLVECT_5:def 1; :: thesis: verum