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) = (dist_cart2S (X,Y)) . (y,x)
let x, y be Element of [: the carrier of X, the carrier of Y:]; :: thesis: (dist_cart2S (X,Y)) . (x,y) = (dist_cart2S (X,Y)) . (y,x)
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] ) ;
then (dist_cart2S (X,Y)) . (x,y) = sqrt (((dist (y1,x1)) ^2) + ((dist (x2,y2)) ^2)) by Def10
.= (dist_cart2S (X,Y)) . (y,x) by A1, Def10 ;
hence (dist_cart2S (X,Y)) . (x,y) = (dist_cart2S (X,Y)) . (y,x) ; :: thesis: verum