theorem :: EUCLID_7:46

for n being Nat holds dim (RealVectSpace (Seg n)) = n