let X, Y, Z be non empty MetrSpace; for x, y being Element of [: the carrier of X, the carrier of Y, the carrier of Z:] holds (dist_cart3S (X,Y,Z)) . (x,y) = (dist_cart3S (X,Y,Z)) . (y,x)
let x, y be Element of [: the carrier of X, the carrier of Y, the carrier of Z:]; (dist_cart3S (X,Y,Z)) . (x,y) = (dist_cart3S (X,Y,Z)) . (y,x)
reconsider x1 = x `1_3 , y1 = y `1_3 as Element of X ;
reconsider x2 = x `2_3 , y2 = y `2_3 as Element of Y ;
reconsider x3 = x `3_3 , y3 = y `3_3 as Element of Z ;
A1:
( x = [x1,x2,x3] & y = [y1,y2,y3] )
;
then (dist_cart3S (X,Y,Z)) . (x,y) =
sqrt ((((dist (y1,x1)) ^2) + ((dist (y2,x2)) ^2)) + ((dist (y3,x3)) ^2))
by Def13
.=
(dist_cart3S (X,Y,Z)) . (y,x)
by A1, Def13
;
hence
(dist_cart3S (X,Y,Z)) . (x,y) = (dist_cart3S (X,Y,Z)) . (y,x)
; verum