theorem Th15: :: ASCOLI:15

for T being NormedLinearTopSpace
for RNS being RealNormSpace st RNS = NORMSTR(# the carrier of T, the ZeroF of T, the U5 of T, the U7 of T, the normF of T #) & the topology of T = the topology of (TopSpaceNorm RNS) holds
( distance_by_norm_of RNS = distance_by_norm_of T & MetricSpaceNorm RNS = MetricSpaceNorm T & TopSpaceNorm T = TopSpaceNorm RNS )