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

assume A2: (dist_cart3S X,Y,Z) . x,y = 0 ; :: thesis:
set d1 = dist x1,y1;
set d2 = dist x2,y2;
set d3 = dist x3,y3;
sqrt ((((dist x1,y1) ^2 ) + ((dist x2,y2) ^2 )) + ((dist x3,y3) ^2 )) = 0 by A1, A2, Def4;
then A3: sqrt (((dist x1,y1) ^2 ) + (((dist x2,y2) ^2 ) + ((dist x3,y3) ^2 ))) = 0 ;
A4: 0 <= (dist x1,y1) ^2 by XREAL_1:65;
A5: 0 <= (dist x2,y2) ^2 by XREAL_1:65;
0 <= (dist x3,y3) ^2 by XREAL_1:65;
then A6: 0 + 0 <= ((dist x2,y2) ^2 ) + ((dist x3,y3) ^2 ) by A5, XREAL_1:9;
then ( (dist x1,y1) ^2 = 0 & ((dist x2,y2) ^2 ) + ((dist x3,y3) ^2 ) = 0 ) by A3, A4, Th2;
then dist x1,y1 = 0 ;
then A7: x1 = y1 by METRIC_1:2;
A8: ((dist x2,y2) ^2 ) + ((dist x3,y3) ^2 ) = 0 by A3, A4, A6, Th2;
A9: 0 <= (dist x2,y2) ^2 by XREAL_1:65;
A10: 0 <= (dist x3,y3) ^2 by XREAL_1:65;
then A11: ( (dist x2,y2) ^2 = 0 & (dist x3,y3) ^2 = 0 ) by A8, A9, XREAL_1:29;
(dist x2,y2) ^2 = 0 by A8, A9, A10, XREAL_1:29;
then dist x2,y2 = 0 ;
then A12: x2 = y2 by METRIC_1:2;
dist x3,y3 = 0 by A11;
hence x = y by A1, A7, A12, METRIC_1:2; :: thesis:

end;

assume A13: x = y ; :: thesis:
then A14: (dist x1,y1) ^2 = 0 ^2 by METRIC_1:1;
A15: (dist x2,y2) ^2 = 0 ^2 by A13, METRIC_1:1;
(dist_cart3S X,Y,Z) . x,y = sqrt ((((dist x1,y1) ^2 ) + ((dist x2,y2) ^2 )) + ((dist x3,y3) ^2 )) by A1, Def4
.= 0 ^2 by A13, A14, A15, METRIC_1:1, SQUARE_1:82 ;
hence (dist_cart3S X,Y,Z) . x,y = 0 ; :: thesis: