let n be Nat; :: thesis: for p, q being POINT of (TarskiEuclidSpace n)
for p1, q1 being Element of (TOP-REAL n) st p = p1 & q = q1 holds
( dist (p,q) = (Pitag_dist n) . (p1,q1) & dist (p,q) = |.(p1 - q1).| )
let p, q be POINT of (TarskiEuclidSpace n); :: thesis: for p1, q1 being Element of (TOP-REAL n) st p = p1 & q = q1 holds
( dist (p,q) = (Pitag_dist n) . (p1,q1) & dist (p,q) = |.(p1 - q1).| )
let p1, q1 be Element of (TOP-REAL n); :: thesis: ( p = p1 & q = q1 implies ( dist (p,q) = (Pitag_dist n) . (p1,q1) & dist (p,q) = |.(p1 - q1).| ) )
assume A0: ( p = p1 & q = q1 ) ; :: thesis: ( dist (p,q) = (Pitag_dist n) . (p1,q1) & dist (p,q) = |.(p1 - q1).| )
A1: MetrStruct(# the U1 of (TarskiEuclidSpace n), the distance of (TarskiEuclidSpace n) #) = MetrStruct(# the U1 of (Euclid n), the distance of (Euclid n) #) by GTARSKI1:def 13;
then (Pitag_dist n) . (p1,q1) = |.(p1 - q1).| by A0, EUCLID:def 6;
hence ( dist (p,q) = (Pitag_dist n) . (p1,q1) & dist (p,q) = |.(p1 - q1).| ) by A1, METRIC_1:def 1, A0; :: thesis: verum