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

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