let x, y be Point of RealSpace; ex xr, yr being Real st
( x = xr & y = yr & dist (x,y) = real_dist . (x,y) & dist (x,y) = (Pitag_dist 1) . (<*x*>,<*y*>) & dist (x,y) = |.(xr - yr).| )
reconsider xr = x, yr = y as Real ;
A1:
real_dist . (x,y) = |.(xr - yr).|
by METRIC_1:def 12;
reconsider x2 = <*xr*>, y2 = <*yr*> as Element of REAL 1 ;
( x2 . 1 = xr & y2 . 1 = yr )
by FINSEQ_1:def 8;
then
(Pitag_dist 1) . (<*x*>,<*y*>) = |.(xr - yr).|
by SRINGS_5:99;
hence
ex xr, yr being Real st
( x = xr & y = yr & dist (x,y) = real_dist . (x,y) & dist (x,y) = (Pitag_dist 1) . (<*x*>,<*y*>) & dist (x,y) = |.(xr - yr).| )
by A1; verum