let n be Element of NAT ; :: thesis: for p1, p2 being Point of
for x1, x2 being Point of st x1 = p1 & x2 = p2 holds
|.(p1 - p2).| = dist x1,x2
let p1, p2 be Point of ; :: thesis: for x1, x2 being Point of st x1 = p1 & x2 = p2 holds
|.(p1 - p2).| = dist x1,x2
let x1, x2 be Point of ; :: 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 ;
(Pitag_dist n) . x1',x2' = |.(x1' - x2').| by EUCLID:def 6
.= |.(p1 - p2).| by A1, EUCLID:73 ;
hence |.(p1 - p2).| = dist x1,x2 by METRIC_1:def 1; :: thesis: verum