let x, y be Point of (TopSpaceMetr (Euclid 1)); :: 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) = (Pitag_dist 1) . (<*xr*>,<*yr*>) & dist (x1,y1) = |.(xr - yr).| )

reconsider xr1 = x as Point of (Euclid 1) ;

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 (Euclid 1) ;

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: (Pitag_dist 1) . (<*r1*>,<*r2*>) = |.((x2 . 1) - (y2 . 1)).| by SRINGS_5:99

.= |.(r1 - r2).| by A3, FINSEQ_1:def 8 ;

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) = (Pitag_dist 1) . (<*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) = (Pitag_dist 1) . (<*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) = (Pitag_dist 1) . (<*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) = (Pitag_dist 1) . (<*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) = (Pitag_dist 1) . (<*r1*>,<*r2*>) & dist (xr2,yr2) = |.(r1 - r2).| ) by A4, A1, A2, METRIC_1:def 12; :: thesis: verum

( x1 = xr & y1 = yr & x = <*xr*> & y = <*yr*> & dist (x1,y1) = real_dist . (xr,yr) & dist (x1,y1) = (Pitag_dist 1) . (<*xr*>,<*yr*>) & dist (x1,y1) = |.(xr - yr).| )

reconsider xr1 = x as Point of (Euclid 1) ;

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 (Euclid 1) ;

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: (Pitag_dist 1) . (<*r1*>,<*r2*>) = |.((x2 . 1) - (y2 . 1)).| by SRINGS_5:99

.= |.(r1 - r2).| by A3, FINSEQ_1:def 8 ;

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) = (Pitag_dist 1) . (<*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) = (Pitag_dist 1) . (<*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) = (Pitag_dist 1) . (<*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) = (Pitag_dist 1) . (<*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) = (Pitag_dist 1) . (<*r1*>,<*r2*>) & dist (xr2,yr2) = |.(r1 - r2).| ) by A4, A1, A2, METRIC_1:def 12; :: thesis: verum