let N be 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 ;
hence |.(p1 - p2).| = dist (x1,x2) by METRIC_1:def 1; :: thesis: verum