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

proof

set d2 = dist (x2,y2);
set d1 = dist (x1,y1);
assume (dist_cart2S (X,Y)) . (x,y) = 0 ; :: thesis: x = y
then A2: sqrt (((dist (x1,y1)) ^2) + ((dist (x2,y2)) ^2)) = 0 by A1, Def10;
A3: ( 0 <= (dist (x1,y1)) ^2 & 0 <= (dist (x2,y2)) ^2 ) by XREAL_1:63;
then dist (x1,y1) = 0 by A2, Lm1;
then A4: x1 = y1 by METRIC_1:2;
dist (x2,y2) = 0 by A2, A3, Lm1;
hence x = y by A1, A4, METRIC_1:2; :: thesis: verum

end;

assume x = y ; :: thesis: (dist_cart2S (X,Y)) . (x,y) = 0
then A5: ( (dist (x1,y1)) ^2 = 0 ^2 & (dist (x2,y2)) ^2 = 0 ^2 ) by METRIC_1:1;
(dist_cart2S (X,Y)) . (x,y) = sqrt (((dist (x1,y1)) ^2) + ((dist (x2,y2)) ^2)) by A1, Def10
.= 0 by A5 ;
hence (dist_cart2S (X,Y)) . (x,y) = 0 ; :: thesis: verum