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 by MCART_1:10;
reconsider x2 = x `2 , y2 = y `2 as Element of Y by MCART_1:10;
A1: ( x = [x1,x2] & y = [y1,y2] ) by MCART_1:24;
then (dist_cart2S X,Y) . x,y = sqrt (((dist y1,x1) ^2 ) + ((dist x2,y2) ^2 )) by Def1
.= (dist_cart2S X,Y) . y,x by A1, Def1 ;
hence (dist_cart2S X,Y) . x,y = (dist_cart2S X,Y) . y,x ; :: thesis: verum