let n be Nat; :: thesis: RN_Base n is Basis of TOP-REAL n
set A = RN_Base n;
set T = TOP-REAL n;
RN_Base n c= REAL n ;
then A1: RN_Base n c= the carrier of (TOP-REAL n) by EUCLID:22;
reconsider A = RN_Base n as finite Subset of (TOP-REAL n) by EUCLID:22;
reconsider B = RN_Base n as Subset of (RealVectSpace (Seg n)) by A1, Lm1;
B is Basis of RealVectSpace (Seg n) by EUCLID_7:45;
then B is linearly-independent by RLVECT_3:def 3;
then A2: A is linearly-independent by Th21;
reconsider V1 = (Omega). (TOP-REAL n) as RealLinearSpace ;
for v being VECTOR of (TOP-REAL n) st v in Lin A holds
v in V1

proof

let v be VECTOR of (TOP-REAL n); :: thesis: ( v in Lin A implies v in V1 )
assume v in Lin A ; :: thesis: v in V1
v in RLSStruct(# the carrier of (TOP-REAL n), the ZeroF of (TOP-REAL n), the U5 of (TOP-REAL n), the Mult of (TOP-REAL n) #) ;
hence v in V1 by RLSUB_1:def 4; :: thesis: verum

end;

then reconsider X = Lin A as Subspace of V1 by RLSUB_1:29;
for x being object holds
( x in the carrier of X iff x in the carrier of V1 )

proof

let x be object ; :: thesis: ( x in the carrier of X iff x in the carrier of V1 )

hereby :: thesis: ( x in the carrier of V1 implies x in the carrier of X )

assume x in the carrier of X ; :: thesis: x in the carrier of V1
then x in X ;
then x in V1 by RLSUB_1:9;
hence x in the carrier of V1 ; :: thesis: verum

end;

assume x in the carrier of V1 ; :: thesis: x in the carrier of X
then x in RLSStruct(# the carrier of (TOP-REAL n), the ZeroF of (TOP-REAL n), the U5 of (TOP-REAL n), the Mult of (TOP-REAL n) #) by RLSUB_1:def 4;
then reconsider x0 = x as Element of (TOP-REAL n) ;
ex l being Linear_Combination of A st x0 = Sum l by Th22;
then x in { (Sum l) where l is Linear_Combination of A : verum } ;
hence x in the carrier of X by RLVECT_3:def 2; :: thesis: verum

end;

then Lin A = (Omega). (TOP-REAL n) by TARSKI:2, EUCLID_7:9;
then Lin A = RLSStruct(# the carrier of (TOP-REAL n), the ZeroF of (TOP-REAL n), the U5 of (TOP-REAL n), the Mult of (TOP-REAL n) #) by RLSUB_1:def 4;
hence RN_Base n is Basis of TOP-REAL n by A2, RLVECT_3:def 3; :: thesis: verum