let X, Y be non empty MetrSpace; :: thesis: for x, y being Element of [:the carrier of X,the carrier of Y:] holds
( (dist_cart2 X,Y) . x,y = 0 iff x = y )
let x, y be Element of [:the carrier of X,the carrier of Y:]; :: thesis: ( (dist_cart2 X,Y) . x,y = 0 iff x = y )
reconsider x1 = x `1 , y1 = y `1 as Element of X by MCART_1:10;
reconsider x2 = x `2 , y2 = y `2 as Element of Y by MCART_1:10;
A1: ( x = [x1,x2] & y = [y1,y2] ) by MCART_1:24;
thus ( (dist_cart2 X,Y) . x,y = 0 implies x = y ) :: thesis: ( x = y implies (dist_cart2 X,Y) . x,y = 0 )

proof

assume A2: (dist_cart2 X,Y) . x,y = 0 ; :: thesis: x = y
set d1 = dist x1,y1;
set d2 = dist x2,y2;
A3: (dist x1,y1) + (dist x2,y2) = 0 by A1, A2, Def1;
A4: 0 <= dist x1,y1 by METRIC_1:5;
0 <= dist x2,y2 by METRIC_1:5;
then A5: ( dist x1,y1 = 0 & dist x2,y2 = 0 ) by A3, A4, XREAL_1:29;
then x1 = y1 by METRIC_1:2;
hence x = y by A1, A5, METRIC_1:2; :: thesis: verum

end;

assume A6: x = y ; :: thesis: (dist_cart2 X,Y) . x,y = 0
then A7: dist x2,y2 = 0 by METRIC_1:1;
(dist_cart2 X,Y) . x,y = (dist x1,y1) + (dist x2,y2) by A1, Def1
.= 0 by A6, A7, METRIC_1:1 ;
hence (dist_cart2 X,Y) . x,y = 0 ; :: thesis: verum