let x, y be Point of (); :: thesis: ex x1, y1 being Point of RealSpace ex xr, yr being Real st
( x1 = xr & y1 = yr & x = <*xr*> & y = <*yr*> & dist (x1,y1) = real_dist . (xr,yr) & dist (x1,y1) = () . (<*xr*>,<*yr*>) & dist (x1,y1) = |.(xr - yr).| )

reconsider xr1 = x as Point of () ;
xr1 in 1 -tuples_on REAL ;
then xr1 in { <*r*> where r is Element of REAL : verum } by FINSEQ_2:96;
then consider r1 being Element of REAL such that
A1: xr1 = <*r1*> ;
reconsider yr1 = y as Point of () ;
yr1 in 1 -tuples_on REAL ;
then yr1 in { <*r*> where r is Element of REAL : verum } by FINSEQ_2:96;
then consider r2 being Element of REAL such that
A2: yr1 = <*r2*> ;
reconsider xr2 = r1, yr2 = r2 as Element of RealSpace ;
reconsider x2 = <*r1*>, y2 = <*r2*> as Element of REAL 1 ;
A3: x2 . 1 = r1 by FINSEQ_1:def 8;
A4: () . (<*r1*>,<*r2*>) = |.((x2 . 1) - (y2 . 1)).| by SRINGS_5:99
.= |.(r1 - r2).| by ;
take xr2 ; :: thesis: ex y1 being Point of RealSpace ex xr, yr being Real st
( xr2 = xr & y1 = yr & x = <*xr*> & y = <*yr*> & dist (xr2,y1) = real_dist . (xr,yr) & dist (xr2,y1) = () . (<*xr*>,<*yr*>) & dist (xr2,y1) = |.(xr - yr).| )

take yr2 ; :: thesis: ex xr, yr being Real st
( xr2 = xr & yr2 = yr & x = <*xr*> & y = <*yr*> & dist (xr2,yr2) = real_dist . (xr,yr) & dist (xr2,yr2) = () . (<*xr*>,<*yr*>) & dist (xr2,yr2) = |.(xr - yr).| )

take r1 ; :: thesis: ex yr being Real st
( xr2 = r1 & yr2 = yr & x = <*r1*> & y = <*yr*> & dist (xr2,yr2) = real_dist . (r1,yr) & dist (xr2,yr2) = () . (<*r1*>,<*yr*>) & dist (xr2,yr2) = |.(r1 - yr).| )

take r2 ; :: thesis: ( xr2 = r1 & yr2 = r2 & x = <*r1*> & y = <*r2*> & dist (xr2,yr2) = real_dist . (r1,r2) & dist (xr2,yr2) = () . (<*r1*>,<*r2*>) & dist (xr2,yr2) = |.(r1 - r2).| )
thus ( xr2 = r1 & yr2 = r2 & x = <*r1*> & y = <*r2*> & dist (xr2,yr2) = real_dist . (r1,r2) & dist (xr2,yr2) = () . (<*r1*>,<*r2*>) & dist (xr2,yr2) = |.(r1 - r2).| ) by ; :: thesis: verum