theorem :: NEURONS1:24

for RNS being RealNormSpace st RNS is finite-dimensional holds
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 )