let x, y be Point of (Euclid 1); :: thesis: for r, s being Real st x = <*r*> & y = <*s*> holds
dist (x,y) = |.(r - s).|
let r, s be Real; :: thesis: ( x = <*r*> & y = <*s*> implies dist (x,y) = |.(r - s).| )
assume that
A1: x = <*r*> and
A2: y = <*s*> ; :: thesis: dist (x,y) = |.(r - s).|
consider x1, y1 being Point of RealSpace, xr, yr being Real such that
x1 = xr and
y1 = yr and
A3: x = <*xr*> and
A4: y = <*yr*> and
dist (x1,y1) = real_dist . (xr,yr) and
A5: dist (x1,y1) = (Pitag_dist 1) . (<*xr*>,<*yr*>) and
A6: dist (x1,y1) = |.(xr - yr).| by Th7;
( xr = r & yr = s ) by A3, A1, A2, A4, FINSEQ_1:76;
hence dist (x,y) = |.(r - s).| by A5, A6, A3, A4; :: thesis: verum