let n be non empty Nat; :: thesis: ( 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) )
set V = n -VectSp_over F_Real;
set W = TOP-REAL n;
thus the carrier of (TOP-REAL n) = the carrier of (n -VectSp_over F_Real) by Lm1; :: thesis: ( 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) )
A1: n -Group_over F_Real = addLoopStr(# (n -tuples_on the carrier of F_Real),(product ( the addF of F_Real,n)),(n |-> (0. F_Real)) #) by PRVECT_1:def 3;
A2: ( addLoopStr(# the carrier of (n -VectSp_over F_Real), the addF of (n -VectSp_over F_Real), the ZeroF of (n -VectSp_over F_Real) #) = n -Group_over F_Real & the lmult of (n -VectSp_over F_Real) = n -Mult_over F_Real ) by PRVECT_1:def 5;
A3: RLSStruct(# the carrier of (TOP-REAL n), the ZeroF of (TOP-REAL n), the addF of (TOP-REAL n), the Mult of (TOP-REAL n) #) = RealVectSpace (Seg n) by EUCLID:def 8;
thus 0. (TOP-REAL n) = 0* n by EUCLID:70
.= 0. (n -VectSp_over F_Real) by A1, A2 ; :: thesis: ( 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) )
thus the addF of (TOP-REAL n) = the addF of (n -VectSp_over F_Real) by A1, A2, A3, Th51; :: thesis: the Mult of (TOP-REAL n) = the lmult of (n -VectSp_over F_Real)
thus the Mult of (TOP-REAL n) = n -Mult_over F_Real by A3, Th52
.= the lmult of (n -VectSp_over F_Real) by PRVECT_1:def 5 ; :: thesis: verum