theorem Th23: :: NEURONS1:23

for RNS being RealNormSpace 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 #)