theorem Th15: :: COUSIN:21

for n being Nat holds MetricSpaceNorm (REAL-NS n) = Euclid n