for x, y being Element of REAL 1 holds (Pitag_dist 1) . (x,y) = |.((x . 1) - (y . 1)).|