let x, y be Element of [:REAL,REAL:]; :: thesis: ( taxi_dist2 . (x,y) = 0 iff x = y )
reconsider x1 = x `1 , x2 = x `2 , y1 = y `1 , y2 = y `2 as Element of REAL ;
A1: ( x = [x1,x2] & y = [y1,y2] ) ;
thus ( taxi_dist2 . (x,y) = 0 implies x = y ) :: thesis: ( x = y implies taxi_dist2 . (x,y) = 0 )

proof

set d2 = real_dist . (x2,y2);
set d1 = real_dist . (x1,y1);
real_dist . (x1,y1) = |.(x1 - y1).| by METRIC_1:def 12;
then A2: 0 <= real_dist . (x1,y1) by COMPLEX1:46;
real_dist . (x2,y2) = |.(x2 - y2).| by METRIC_1:def 12;
then A3: 0 <= real_dist . (x2,y2) by COMPLEX1:46;
assume taxi_dist2 . (x,y) = 0 ; :: thesis: x = y
then A4: (real_dist . (x1,y1)) + (real_dist . (x2,y2)) = 0 by A1, Def16;
then real_dist . (x1,y1) = 0 by A2, A3, XREAL_1:27;
then A5: x1 = y1 by METRIC_1:8;
real_dist . (x2,y2) = 0 by A4, A2, A3, XREAL_1:27;
hence x = y by A1, A5, METRIC_1:8; :: thesis: verum

end;

assume A6: x = y ; :: thesis: taxi_dist2 . (x,y) = 0
then A7: real_dist . (x2,y2) = 0 by METRIC_1:8;
taxi_dist2 . (x,y) = (real_dist . (x1,y1)) + (real_dist . (x2,y2)) by A1, Def16
.= 0 by A6, A7, METRIC_1:8 ;
hence taxi_dist2 . (x,y) = 0 ; :: thesis: verum