theorem Th54: :: REAL_NS2:54

for n being non empty Nat holds
( the carrier of (TOP-REAL n) = the carrier of (n -VectSp_over F_Real) & 0. (TOP-REAL n) = 0. (n -VectSp_over F_Real) & the addF of (TOP-REAL n) = the addF of (n -VectSp_over F_Real) & the Mult of (TOP-REAL n) = the lmult of (n -VectSp_over F_Real) )