theorem Th83: :: REAL_NS2:83

for n being non empty Nat holds RLSp2RVSp (RealVectSpace (Seg n)) = n -VectSp_over F_Real