theorem Th66: :: SRINGS_5:99

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