let T be NormedLinearTopSpace; :: thesis: for RNS being RealNormSpace st T is finite-dimensional & RNS = NORMSTR(# the carrier of T, the ZeroF of T, the addF of T, the Mult of T, the normF of T #) holds
( RNS is finite-dimensional & dim RNS = dim T )
let RNS be RealNormSpace; :: thesis: ( T is finite-dimensional & RNS = NORMSTR(# the carrier of T, the ZeroF of T, the addF of T, the Mult of T, the normF of T #) implies ( RNS is finite-dimensional & dim RNS = dim T ) )
assume A1: ( T is finite-dimensional & RNS = NORMSTR(# the carrier of T, the ZeroF of T, the addF of T, the Mult of T, the normF of T #) ) ; :: thesis: ( RNS is finite-dimensional & dim RNS = dim T )
then RLSStruct(# the carrier of T, the ZeroF of T, the addF of T, the Mult of T #) = RLSStruct(# the carrier of RNS, the ZeroF of RNS, the addF of RNS, the Mult of RNS #) ;
hence ( RNS is finite-dimensional & dim RNS = dim T ) by Th21, A1; :: thesis: verum