for n being Nat
for r being Real st r > 0 holds
for x, y, z being Element of (Euclid n) st x = 0* n holds
for p being Element of (TOP-REAL n) st p = y & r * p = z holds
r * (dist (x,y)) = dist (x,z) by Lm1;