let RNS1, RNS2 be RealLinearSpace; :: thesis: ( RLSStruct(# the carrier of RNS1, the ZeroF of RNS1, the addF of RNS1, the Mult of RNS1 #) = RLSStruct(# the carrier of RNS2, the ZeroF of RNS2, the addF of RNS2, the Mult of RNS2 #) implies for X being object holds
( X is Subspace of RNS2 iff X is Subspace of RNS1 ) )
assume A1: RLSStruct(# the carrier of RNS1, the ZeroF of RNS1, the addF of RNS1, the Mult of RNS1 #) = RLSStruct(# the carrier of RNS2, the ZeroF of RNS2, the addF of RNS2, the Mult of RNS2 #) ; :: thesis: for X being object holds
( X is Subspace of RNS2 iff X is Subspace of RNS1 )
let X be object ; :: thesis: ( X is Subspace of RNS2 iff X is Subspace of RNS1 )

hereby :: thesis: ( X is Subspace of RNS1 implies X is Subspace of RNS2 )

assume X is Subspace of RNS2 ; :: thesis: X is Subspace of RNS1
then reconsider V = X as Subspace of RNS2 ;
A2: ( the carrier of V c= the carrier of RNS2 & 0. V = 0. RNS2 & the addF of V = the addF of RNS2 || the carrier of V & the Mult of V = the Mult of RNS2 | [:REAL, the carrier of V:] ) by RLSUB_1:def 2;
0. V = 0. RNS1 by A2, A1;
hence X is Subspace of RNS1 by A1, A2, RLSUB_1:def 2; :: thesis: verum

end;

assume X is Subspace of RNS1 ; :: thesis: X is Subspace of RNS2
then reconsider V = X as Subspace of RNS1 ;
A4: ( the carrier of V c= the carrier of RNS1 & 0. V = 0. RNS1 & the addF of V = the addF of RNS1 || the carrier of V & the Mult of V = the Mult of RNS1 | [:REAL, the carrier of V:] ) by RLSUB_1:def 2;
0. V = 0. RNS2 by A4, A1;
hence X is Subspace of RNS2 by A1, A4, RLSUB_1:def 2; :: thesis: verum