let n be Nat; :: thesis: Euclid n = MetricSpaceNorm (REAL-NS n)
set X = REAL-NS n;
A1: the carrier of (Euclid n) = the carrier of (REAL-NS n) by REAL_NS1:def 4;
for x, y being Element of REAL n holds the distance of (Euclid n) . (x,y) = (distance_by_norm_of (REAL-NS n)) . (x,y)

proof

let x, y be Element of REAL n; :: thesis: the distance of (Euclid n) . (x,y) = (distance_by_norm_of (REAL-NS n)) . (x,y)
reconsider x1 = x, y1 = y as Point of (REAL-NS n) by REAL_NS1:def 4;
thus the distance of (Euclid n) . (x,y) = |.(x - y).| by EUCLID:def 6
.= ||.(x1 - y1).|| by REAL_NS1:1, REAL_NS1:5
.= (distance_by_norm_of (REAL-NS n)) . (x,y) by NORMSP_2:def 1 ; :: thesis: verum

end;

hence Euclid n = MetricSpaceNorm (REAL-NS n) by BINOP_1:2, A1; :: thesis: verum