let x, y be Point of RealSpace; :: thesis: 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; :: thesis: verum