theorem Th15: :: COUSIN:19

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