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 x1' = x1, x2' = x2 as Element of REAL n ;
X: p1 - p2 = x1' - x2' by A1, EUCLID:73;
(Pitag_dist n) . x1',x2' = |.(x1' - x2').| by A1, EUCLID:def 6
.= |.(p1 - p2).| by A1, X, EUCLID:68 ;
hence |.(p1 - p2).| = dist x1,x2 by METRIC_1:def 1; :: thesis: verum