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