theorem Th62: :: REAL_NS2:62

for n being Nat holds
( REAL-NS n is finite-dimensional & dim (REAL-NS n) = n )