let n be Nat; :: thesis: the carrier of (n -VectSp_over F_Real) = the carrier of (REAL-NS n)
thus the carrier of (n -VectSp_over F_Real) = the carrier of (TOP-REAL n) by Lm2
.= the carrier of (REAL-NS n) by Th4 ; :: thesis: verum