theorem Th21: :: NEURONS1:21

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 #) & RNS1 is finite-dimensional holds
( RNS2 is finite-dimensional & dim RNS2 = dim RNS1 )