let n be Nat; :: thesis: for x, y being Element of (Euclid n)
for g, h being Point of (REAL-NS n) st x = g & y = h holds
dist (x,y) = ||.(g - h).||
let x, y be Element of (Euclid n); :: thesis: for g, h being Point of (REAL-NS n) st x = g & y = h holds
dist (x,y) = ||.(g - h).||
let g, h be Point of (REAL-NS n); :: thesis: ( x = g & y = h implies dist (x,y) = ||.(g - h).|| )
assume A1: ( x = g & y = h ) ; :: thesis: dist (x,y) = ||.(g - h).||
( x in Euclid n & y in Euclid n ) ;
then ( x in TOP-REAL n & y in TOP-REAL n ) by EUCLID:67;
then reconsider rx = x, ry = y as Element of REAL n by EUCLID:22;
A2: Euclid n = MetrStruct(# (REAL n),(Pitag_dist n) #) by EUCLID:def 7;
reconsider g1 = g, h1 = h as Element of REAL n by REAL_NS1:def 4;
reconsider z1 = g1 - h1 as Element of REAL n ;
||.(g - h).|| = the normF of (REAL-NS n) . (g1 - h1) by REAL_NS1:5
.= (Euclid_norm n) . z1 by REAL_NS1:def 4
.= |.z1.| by REAL_NS1:def 3 ;
hence dist (x,y) = ||.(g - h).|| by A1, A2, EUCLID:def 6; :: thesis: verum