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 , 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 ;
reconsider x4 = x `4 , y4 = y `4 as Element of W ;
A1: ( x = [x1,x2,x3,x4] & y = [y1,y2,y3,y4] ) by MCART_1:60;
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