let RNS be RealNormSpace; :: thesis: ( RNS is finite-dimensional implies ex T being NormedLinearTopSpace st
( NORMSTR(# the carrier of RNS, the ZeroF of RNS, the addF of RNS, the Mult of RNS, the normF of RNS #) = NORMSTR(# the carrier of T, the ZeroF of T, the addF of T, the Mult of T, the normF of T #) & T is finite-dimensional ) )
assume A1: RNS is finite-dimensional ; :: thesis: ex T being NormedLinearTopSpace st
( NORMSTR(# the carrier of RNS, the ZeroF of RNS, the addF of RNS, the Mult of RNS, the normF of RNS #) = NORMSTR(# the carrier of T, the ZeroF of T, the addF of T, the Mult of T, the normF of T #) & T is finite-dimensional )
consider T being NormedLinearTopSpace such that
A2: NORMSTR(# the carrier of RNS, the ZeroF of RNS, the addF of RNS, the Mult of RNS, the normF of RNS #) = NORMSTR(# the carrier of T, the ZeroF of T, the addF of T, the Mult of T, the normF of T #) by Th23;
take T ; :: thesis: ( NORMSTR(# the carrier of RNS, the ZeroF of RNS, the addF of RNS, the Mult of RNS, the normF of RNS #) = NORMSTR(# the carrier of T, the ZeroF of T, the addF of T, the Mult of T, the normF of T #) & T is finite-dimensional )
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 #) by A2;
hence ( NORMSTR(# the carrier of RNS, the ZeroF of RNS, the addF of RNS, the Mult of RNS, the normF of RNS #) = NORMSTR(# the carrier of T, the ZeroF of T, the addF of T, the Mult of T, the normF of T #) & T is finite-dimensional ) by Th21, A1, A2; :: thesis: verum