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 #) & RNS1 is finite-dimensional implies ( RNS2 is finite-dimensional & dim RNS2 = dim 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 #) & RNS1 is finite-dimensional ) ; :: thesis: ( RNS2 is finite-dimensional & dim RNS2 = dim RNS1 )
then consider A being finite Subset of RNS1 such that
A2: A is Basis of RNS1 by RLVECT_5:def 1;
A3: dim RNS1 = card A by RLVECT_5:def 2, A2, A1;
reconsider B = A as finite Subset of RNS2 by A1;
A4: B is Basis of RNS2 by Th20, A1, A2;
hence RNS2 is finite-dimensional by RLVECT_5:def 1; :: thesis: dim RNS2 = dim RNS1
hence dim RNS2 = dim RNS1 by RLVECT_5:def 2, A3, A4; :: thesis: verum