let n be Nat; :: thesis: distance_by_norm_of (REAL-NS n) = Pitag_dist n
the carrier of (REAL-NS n) = REAL n by REAL_NS1:def 4;
then reconsider d1 = distance_by_norm_of (REAL-NS n) as Function of [:(REAL n),(REAL n):],REAL ;

now :: thesis: for x, y being set st x in REAL n & y in REAL n holds
(Pitag_dist n) . (x,y) = d1 . (x,y)

let x, y be set ; :: thesis: ( x in REAL n & y in REAL n implies (Pitag_dist n) . (x,y) = d1 . (x,y) )
assume A1: ( x in REAL n & y in REAL n ) ; :: thesis: (Pitag_dist n) . (x,y) = d1 . (x,y)
then ( x is Element of (TOP-REAL n) & y is Element of (TOP-REAL n) ) by EUCLID:22;
then reconsider px = x, py = y as Element of (Euclid n) by EUCLID:67;
reconsider g = x, h = y as Point of (REAL-NS n) by A1, REAL_NS1:def 4;
Euclid n = MetrStruct(# (REAL n),(Pitag_dist n) #) by EUCLID:def 7;
hence (Pitag_dist n) . (x,y) = dist (px,py)
.= ||.(g - h).|| by Th9
.= d1 . (x,y) by NORMSP_2:def 1 ;
:: thesis: verum

end;

hence distance_by_norm_of (REAL-NS n) = Pitag_dist n by BINOP_1:def 21; :: thesis: verum