theorem :: NEURONS1:18

for RNS1, RNS2 being RealLinearSpace st 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 #) holds
for X being object holds
( X is Subspace of RNS2 iff X is Subspace of RNS1 )