let x, y be set ; :: thesis:
assume ( x in REAL 1 & y in REAL 1 ) ; :: thesis:
then reconsider x1 = x, y1 = y as Element of REAL 1 ;
thus (Pitag_dist 1) . (x,y) = |.((x1 . 1) - (y1 . 1)).| by Th66
.= (Infty_dist 1) . (x,y) by Th65 ; :: thesis:

end;