let n be Nat; :: thesis: ( TOP-REAL n is finite-dimensional & dim (TOP-REAL n) = n )
set V = n -VectSp_over F_Real;
set W = TOP-REAL n;
A1: dim (n -VectSp_over F_Real) = n by MATRIX13:112;
consider A being finite Subset of (n -VectSp_over F_Real) such that
A2: A is Basis of (n -VectSp_over F_Real) by MATRLIN:def 1;
A3: card A = n by A1, A2, VECTSP_9:def 1;
reconsider B = A as finite Subset of (TOP-REAL n) by Lm1;
thus TOP-REAL n is finite-dimensional ; :: thesis: dim (TOP-REAL n) = n
B is Basis of TOP-REAL n by A2, Th50;
hence dim (TOP-REAL n) = n by A3, RLVECT_5:def 2; :: thesis: verum