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 () by EUCLID:22;
reconsider A = RN_Base n as finite Subset of () by EUCLID:22;
reconsider B = RN_Base n as Subset of (RealVectSpace (Seg n)) by ;
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). () as RealLinearSpace ;
for v being VECTOR of () st v in Lin A holds
v in V1
proof
let v be VECTOR of (); :: thesis: ( v in Lin A implies v in V1 )
assume v in Lin A ; :: thesis: v in V1
v in RLSStruct(# the carrier of (), the ZeroF of (), the U5 of (), the Mult of () #) ;
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 (), the ZeroF of (), the U5 of (), the Mult of () #) by RLSUB_1:def 4;
then reconsider x0 = x as Element of () ;
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). () by ;
then Lin A = RLSStruct(# the carrier of (), the ZeroF of (), the U5 of (), the Mult of () #) by RLSUB_1:def 4;
hence RN_Base n is Basis of TOP-REAL n by ; :: thesis: verum