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