let X, Y, Z be non empty MetrSpace; :: thesis: for x, y being Element of [: the carrier of X, the carrier of Y, the carrier of Z:] holds
( (dist_cart3 (X,Y,Z)) . (x,y) = 0 iff x = y )
let x, y be Element of [: the carrier of X, the carrier of Y, the carrier of Z:]; :: thesis: ( (dist_cart3 (X,Y,Z)) . (x,y) = 0 iff x = y )
reconsider x1 = x `1_3 , y1 = y `1_3 as Element of X ;
reconsider x2 = x `2_3 , y2 = y `2_3 as Element of Y ;
reconsider x3 = x `3_3 , y3 = y `3_3 as Element of Z ;
A1: ( x = [x1,x2,x3] & y = [y1,y2,y3] ) ;
thus ( (dist_cart3 (X,Y,Z)) . (x,y) = 0 implies x = y ) :: thesis: ( x = y implies (dist_cart3 (X,Y,Z)) . (x,y) = 0 )

proof

set d3 = dist (x3,y3);
set d2 = dist (x2,y2);
set d1 = dist (x1,y1);
set d4 = (dist (x1,y1)) + (dist (x2,y2));
assume (dist_cart3 (X,Y,Z)) . (x,y) = 0 ; :: thesis: x = y
then A2: ((dist (x1,y1)) + (dist (x2,y2))) + (dist (x3,y3)) = 0 by A1, Def4;
A3: ( 0 <= dist (x1,y1) & 0 <= dist (x2,y2) ) by METRIC_1:5;
then A4: ( 0 <= dist (x3,y3) & 0 + 0 <= (dist (x1,y1)) + (dist (x2,y2)) ) by METRIC_1:5, XREAL_1:7;
then A5: (dist (x1,y1)) + (dist (x2,y2)) = 0 by A2, XREAL_1:27;
then dist (x1,y1) = 0 by A3, XREAL_1:27;
then A6: x1 = y1 by METRIC_1:2;
dist (x3,y3) = 0 by A2, A4, XREAL_1:27;
then A7: x3 = y3 by METRIC_1:2;
dist (x2,y2) = 0 by A3, A5, XREAL_1:27;
hence x = y by A1, A7, A6, METRIC_1:2; :: thesis: verum

end;

assume A8: x = y ; :: thesis: (dist_cart3 (X,Y,Z)) . (x,y) = 0
then A9: ( dist (x1,y1) = 0 & dist (x2,y2) = 0 ) by METRIC_1:1;
(dist_cart3 (X,Y,Z)) . (x,y) = ((dist (x1,y1)) + (dist (x2,y2))) + (dist (x3,y3)) by A1, Def4
.= 0 by A8, A9, METRIC_1:1 ;
hence (dist_cart3 (X,Y,Z)) . (x,y) = 0 ; :: thesis: verum