let n be Nat; :: thesis: the carrier of (n -VectSp_over F_Real) = the carrier of (TOP-REAL n)

thus the carrier of (n -VectSp_over F_Real) = n -tuples_on the carrier of F_Real by MATRIX13:102

.= REAL n by EUCLID:def 1, VECTSP_1:def 5

.= the carrier of (TOP-REAL n) by EUCLID:22 ; :: thesis: verum

thus the carrier of (n -VectSp_over F_Real) = n -tuples_on the carrier of F_Real by MATRIX13:102

.= REAL n by EUCLID:def 1, VECTSP_1:def 5

.= the carrier of (TOP-REAL n) by EUCLID:22 ; :: thesis: verum