let n be Element of 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