let n be Nat; :: thesis: for u1, u2 being Point of (Euclid n)
for v1, v2 being Element of REAL n st v1 = u1 & v2 = u2 holds
dist (u1,u2) = |.(v1 - v2).|
let u1, u2 be Point of (Euclid n); :: thesis: for v1, v2 being Element of REAL n st v1 = u1 & v2 = u2 holds
dist (u1,u2) = |.(v1 - v2).|
let v1, v2 be Element of REAL n; :: thesis: ( v1 = u1 & v2 = u2 implies dist (u1,u2) = |.(v1 - v2).| )
assume ( v1 = u1 & v2 = u2 ) ; :: thesis: dist (u1,u2) = |.(v1 - v2).|
hence dist (u1,u2) = (Pitag_dist n) . (v1,v2) by METRIC_1:def 1
.= |.(v1 - v2).| by EUCLID:def 6 ;
:: thesis: verum