theorem Th15: :: REAL_NS3:14

for n being Nat holds RLSStruct(# the carrier of (REAL-NS n), the ZeroF of (REAL-NS n), the U5 of (REAL-NS n), the Mult of (REAL-NS n) #) = RealVectSpace (Seg n)