let n be Nat; :: thesis: for X being object holds
( X is Subspace of REAL-NS n iff X is Subspace of TOP-REAL n )
let X be object ; :: thesis: ( X is Subspace of REAL-NS n iff X is Subspace of TOP-REAL n )
A1: the addF of (REAL-NS n) = the addF of 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) #)
.= the addF of 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 Th1
.= the addF of (TOP-REAL n) ;
A2: the Mult of (REAL-NS n) = the Mult of 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) #)
.= the Mult of 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 Th1
.= the Mult of (TOP-REAL n) ;
hereby :: thesis: ( X is Subspace of TOP-REAL n implies X is Subspace of REAL-NS n )
assume X is Subspace of REAL-NS n ; :: thesis: X is Subspace of TOP-REAL n
then reconsider V = X as Subspace of REAL-NS n ;
A3: ( the carrier of V c= the carrier of (REAL-NS n) & 0. V = 0. (REAL-NS n) & the addF of V = the addF of (REAL-NS n) || the carrier of V & the Mult of V = the Mult of (REAL-NS n) | [:REAL, the carrier of V:] ) by RLSUB_1:def 2;
then A4: the carrier of V c= the carrier of (TOP-REAL n) by Th4;
0. V = 0. (TOP-REAL n) by A3, Th6;
hence X is Subspace of TOP-REAL n by A1, A2, A3, A4, RLSUB_1:def 2; :: thesis: verum
end;
assume X is Subspace of TOP-REAL n ; :: thesis: X is Subspace of REAL-NS n
then reconsider V = X as Subspace of TOP-REAL n ;
A5: ( the carrier of V c= the carrier of (TOP-REAL n) & 0. V = 0. (TOP-REAL n) & the addF of V = the addF of (TOP-REAL n) || the carrier of V & the Mult of V = the Mult of (TOP-REAL n) | [:REAL, the carrier of V:] ) by RLSUB_1:def 2;
A6: the carrier of V c= the carrier of (REAL-NS n) by A5, Th4;
0. V = 0. (REAL-NS n) by A5, Th6;
hence X is Subspace of REAL-NS n by A1, A2, A5, A6, RLSUB_1:def 2; :: thesis: verum