let n be Element of NAT ; :: thesis: for p1, p2 being Point of (TOP-REAL n)
for x1, x2 being Point of (Euclid n) st x1 = p1 & x2 = p2 holds
|.(p1 - p2).| = dist (x1,x2)
let p1, p2 be Point of (TOP-REAL n); :: thesis: for x1, x2 being Point of (Euclid n) st x1 = p1 & x2 = p2 holds
|.(p1 - p2).| = dist (x1,x2)
let x1, x2 be Point of (Euclid n); :: thesis: ( x1 = p1 & x2 = p2 implies |.(p1 - p2).| = dist (x1,x2) )
assume A1: ( x1 = p1 & x2 = p2 ) ; :: thesis: |.(p1 - p2).| = dist (x1,x2)
reconsider x19 = x1, x29 = x2 as Element of REAL n ;
(Pitag_dist n) . (x19,x29) = |.(x19 - x29).| by EUCLID:def 6
.= |.(p1 - p2).| by A1, EUCLID:69 ;
hence |.(p1 - p2).| = dist (x1,x2) by METRIC_1:def 1; :: thesis: verum