reconsider B = RN_Base n as Subset of (REAL-US n) by REAL_NS1:def 6;
B is Basis of REAL-US n by Th48;
hence REAL-US n is finite-dimensional by RUSUB_4:def 1; :: thesis: verum