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

( 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