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