let n be Nat; :: thesis: for X being set holds
( X is Basis of TOP-REAL n iff X is Basis of REAL-NS n )
let X be set ; :: thesis: ( X is Basis of TOP-REAL n iff X is Basis of REAL-NS n )
set V = TOP-REAL n;
set W = REAL-NS n;

hereby :: thesis: ( X is Basis of REAL-NS n implies X is Basis of TOP-REAL n )

assume X is Basis of TOP-REAL n ; :: thesis: X is Basis of REAL-NS n
then reconsider A = X as Basis of TOP-REAL n ;
reconsider B = A as Subset of (REAL-NS n) by Th4;
A1: ( A is linearly-independent & Lin A = 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) #) ) by RLVECT_3:def 3;
then A2: B is linearly-independent by Th28;
set W0 = (Omega). (REAL-NS n);
A3: (Omega). (REAL-NS n) = RLSStruct(# the carrier of (REAL-NS n), the ZeroF of (REAL-NS n), the addF of (REAL-NS n), the Mult of (REAL-NS n) #) by RLSUB_1:def 4;
A4: Lin B is strict Subspace of (Omega). (REAL-NS n) by Th49;
A5: [#] (Lin A) = the carrier of (REAL-NS n) by A1, Th4;
the carrier of (Lin B) = [#] (Lin B)
.= the carrier of ((Omega). (REAL-NS n)) by A3, A5, Th26 ;
then Lin B = (Omega). (REAL-NS n) by A4, RLSUB_1:32
.= RLSStruct(# the carrier of (REAL-NS n), the ZeroF of (REAL-NS n), the addF of (REAL-NS n), the Mult of (REAL-NS n) #) by RLSUB_1:def 4 ;
hence X is Basis of REAL-NS n by A2, RLVECT_3:def 3; :: thesis: verum

end;

assume X is Basis of REAL-NS n ; :: thesis: X is Basis of TOP-REAL n
then reconsider A = X as Basis of REAL-NS n ;
reconsider B = A as Subset of (TOP-REAL n) by Th4;
A6: ( A is linearly-independent & Lin A = RLSStruct(# the carrier of (REAL-NS n), the ZeroF of (REAL-NS n), the addF of (REAL-NS n), the Mult of (REAL-NS n) #) ) by RLVECT_3:def 3;
then A7: B is linearly-independent by Th28;
set V0 = (Omega). (TOP-REAL n);
A8: (Omega). (TOP-REAL n) = 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) #) by RLSUB_1:def 4;
A9: Lin B is strict Subspace of (Omega). (TOP-REAL n) by Th49;
A10: [#] (Lin A) = the carrier of (TOP-REAL n) by A6, Th4;
the carrier of (Lin B) = [#] (Lin B)
.= the carrier of ((Omega). (TOP-REAL n)) by A8, A10, Th26 ;
then Lin B = (Omega). (TOP-REAL n) by A9, RLSUB_1:32
.= 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) #) by RLSUB_1:def 4 ;
hence X is Basis of TOP-REAL n by A7, RLVECT_3:def 3; :: thesis: verum