now :: thesis: for x, y being set st x in REAL 1 & y in REAL 1 holds
(Pitag_dist 1) . (x,y) = (Infty_dist 1) . (x,y)

let x, y be set ; :: thesis: ( x in REAL 1 & y in REAL 1 implies (Pitag_dist 1) . (x,y) = (Infty_dist 1) . (x,y) )
assume ( x in REAL 1 & y in REAL 1 ) ; :: thesis: (Pitag_dist 1) . (x,y) = (Infty_dist 1) . (x,y)
then reconsider x1 = x, y1 = y as Element of REAL 1 ;
thus (Pitag_dist 1) . (x,y) = |.((x1 . 1) - (y1 . 1)).| by Th66
.= (Infty_dist 1) . (x,y) by Th65 ; :: thesis: verum

end;

hence Pitag_dist 1 = Infty_dist 1 by BINOP_1:def 21; :: thesis: verum