let n be Nat; :: thesis: MetricSpaceNorm (REAL-NS n) = Euclid n
set MS = MetricSpaceNorm (REAL-NS n);
A1: MetricSpaceNorm (REAL-NS n) = MetrStruct(# the carrier of (REAL-NS n),(distance_by_norm_of (REAL-NS n)) #) by NORMSP_2:def 2;
then A2: the carrier of (MetricSpaceNorm (REAL-NS n)) = REAL n by REAL_NS1:def 4;
Euclid n = MetrStruct(# (REAL n),(Pitag_dist n) #) by EUCLID:def 7;
hence MetricSpaceNorm (REAL-NS n) = Euclid n by A1, A2, Th14; :: thesis: verum