let n be Nat; :: thesis: for p, q being Element of (TarskiEuclidSpace n)
for p1, q1 being Element of (Euclid n) st p = p1 & q = q1 holds
dist (p,q) = dist (p1,q1)
let p, q be Element of (TarskiEuclidSpace n); :: thesis: for p1, q1 being Element of (Euclid n) st p = p1 & q = q1 holds
dist (p,q) = dist (p1,q1)
let p1, q1 be Element of (Euclid n); :: thesis: ( p = p1 & q = q1 implies dist (p,q) = dist (p1,q1) )
assume A1: ( p = p1 & q = q1 ) ; :: thesis: dist (p,q) = dist (p1,q1)
thus dist (p,q) = the distance of MetrStruct(# the U1 of (TarskiEuclidSpace n), the distance of (TarskiEuclidSpace n) #) . (p,q) by METRIC_1:def 1
.= the distance of MetrStruct(# the U1 of (Euclid n), the distance of (Euclid n) #) . (p,q) by GTARSKI1:def 13
.= dist (p1,q1) by METRIC_1:def 1, A1 ; :: thesis: verum