let n be Nat; 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 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 ;
( 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 )
;
(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
;
verum end;
hence
distance_by_norm_of (REAL-NS n) = Pitag_dist n
by BINOP_1:def 21; verum