let n be Element of NAT ; :: thesis: for p, q being Point of (TOP-REAL n)
for p9, q9 being Point of (Euclid n) st p = p9 & q = q9 holds
dist (p9,q9) = |.(p - q).|
let p, q be Point of (TOP-REAL n); :: thesis: for p9, q9 being Point of (Euclid n) st p = p9 & q = q9 holds
dist (p9,q9) = |.(p - q).|
let p9, q9 be Point of (Euclid n); :: thesis: ( p = p9 & q = q9 implies dist (p9,q9) = |.(p - q).| )
assume A1: ( p = p9 & q = q9 ) ; :: thesis: dist (p9,q9) = |.(p - q).|
reconsider pp = p, qq = q as Element of REAL n by EUCLID:22;
dist (p9,q9) = |.(pp - qq).| by A1, Th20;
hence dist (p9,q9) = |.(p - q).| by EUCLID:69; :: thesis: verum