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

for x being object holds

( x in the carrier of X iff x in the carrier of V1 )

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

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

then reconsider X = Lin A as Subspace of V1 by RLSUB_1:29;
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;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

for x being object holds

( x in the carrier of X iff x in the carrier of V1 )

proof

then
Lin A = (Omega). (TOP-REAL n)
by TARSKI:2, EUCLID_7:9;
let x be object ; :: thesis: ( x in the carrier of X iff x in the carrier of V1 )

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;hereby :: thesis: ( x in the carrier of V1 implies x in the carrier of X )

assume
x in the carrier of V1
; :: thesis: x in the carrier of Xassume
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;then x in X ;

then x in V1 by RLSUB_1:9;

hence x in the carrier of V1 ; :: thesis: verum

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

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