let n be Nat; :: thesis: ( REAL-NS n is finite-dimensional & dim (REAL-NS n) = n )
set V = TOP-REAL n;
set W = REAL-NS n;
A1: dim (TOP-REAL n) = n by Th53;
consider A being finite Subset of (TOP-REAL n) such that
A3: A is Basis of TOP-REAL n by RLVECT_5:def 1;
A4: card A = n by A1, A3, RLVECT_5:def 2;
reconsider B = A as finite Subset of (REAL-NS n) by Th4;
A5: B is Basis of REAL-NS n by A3, Th61;
hence REAL-NS n is finite-dimensional by RLVECT_5:def 1; :: thesis: dim (REAL-NS n) = n
hence dim (REAL-NS n) = n by A4, A5, RLVECT_5:def 2; :: thesis: verum