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