let n be non empty Nat; RLSp2RVSp (RealVectSpace (Seg n)) = n -VectSp_over F_Real
set X = RealVectSpace (Seg n);
set V = n -VectSp_over F_Real;
set W = TOP-REAL n;
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;
A5: 0. (RLSp2RVSp (RealVectSpace (Seg n))) =
0. (TOP-REAL n)
by A3
.=
0* n
by EUCLID:70
.=
0. (n -VectSp_over F_Real)
by A1, A2
;
A6:
the addF of (RLSp2RVSp (RealVectSpace (Seg n))) = the addF of (n -VectSp_over F_Real)
by A1, A2, Th51;
the lmult of (RLSp2RVSp (RealVectSpace (Seg n))) =
n -Mult_over F_Real
by Th52
.=
the lmult of (n -VectSp_over F_Real)
by PRVECT_1:def 5
;
hence
RLSp2RVSp (RealVectSpace (Seg n)) = n -VectSp_over F_Real
by A3, A5, A6, Lm1; verum