let X, Y, Z, W be non empty MetrSpace; :: thesis: for x, y being Element of [: the carrier of X, the carrier of Y, the carrier of Z, the carrier of W:] holds (dist_cart4 (X,Y,Z,W)) . (x,y) = (dist_cart4 (X,Y,Z,W)) . (y,x)
let x, y be Element of [: the carrier of X, the carrier of Y, the carrier of Z, the carrier of W:]; :: thesis: (dist_cart4 (X,Y,Z,W)) . (x,y) = (dist_cart4 (X,Y,Z,W)) . (y,x)
reconsider x1 = x `1_4 , y1 = y `1_4 as Element of X ;
reconsider x2 = x `2_4 , y2 = y `2_4 as Element of Y ;
reconsider x3 = x `3_4 , y3 = y `3_4 as Element of Z ;
reconsider x4 = x `4_4 , y4 = y `4_4 as Element of W ;
A1: ( x = [x1,x2,x3,x4] & y = [y1,y2,y3,y4] ) ;
then (dist_cart4 (X,Y,Z,W)) . (x,y) = ((dist (y1,x1)) + (dist (y2,x2))) + ((dist (y3,x3)) + (dist (x4,y4))) by Def7
.= (dist_cart4 (X,Y,Z,W)) . (y,x) by A1, Def7 ;
hence (dist_cart4 (X,Y,Z,W)) . (x,y) = (dist_cart4 (X,Y,Z,W)) . (y,x) ; :: thesis: verum