let T be NormedLinearTopSpace; :: thesis: 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 )
let RNS be RealNormSpace; :: thesis: ( 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) implies ( distance_by_norm_of RNS = distance_by_norm_of T & MetricSpaceNorm RNS = MetricSpaceNorm T & TopSpaceNorm T = TopSpaceNorm RNS ) )
assume A1: ( 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) ) ; :: thesis: ( distance_by_norm_of RNS = distance_by_norm_of T & MetricSpaceNorm RNS = MetricSpaceNorm T & TopSpaceNorm T = TopSpaceNorm RNS )
A2: for x, y being Point of RNS holds (distance_by_norm_of T) . (x,y) = ||.(x - y).||
proof
let x, y be Point of RNS; :: thesis: (distance_by_norm_of T) . (x,y) = ||.(x - y).||
reconsider x1 = x, y1 = y as Point of T by A1;
thus (distance_by_norm_of T) . (x,y) = ||.(x1 - y1).|| by NORMSP_2:def 1
.= ||.(x - y).|| by C0SP3:19, A1 ; :: thesis: verum
end;
hence distance_by_norm_of RNS = distance_by_norm_of T by A1, NORMSP_2:def 1; :: thesis: ( MetricSpaceNorm RNS = MetricSpaceNorm T & TopSpaceNorm T = TopSpaceNorm RNS )
thus MetricSpaceNorm RNS = MetricSpaceNorm T by A2, NORMSP_2:def 1, A1; :: thesis: TopSpaceNorm T = TopSpaceNorm RNS
thus TopSpaceNorm T = TopSpaceNorm RNS by A2, NORMSP_2:def 1, A1; :: thesis: verum