theorem Th2: :: REAL_NS2:2

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