:: deftheorem Def13 defines dist_cart3S METRIC_3:def 13 :
for X, Y, Z being non empty MetrSpace
for b₄ being Function of [:[: the carrier of X, the carrier of Y, the carrier of Z:],[: the carrier of X, the carrier of Y, the carrier of Z:]:],REAL holds
( b₄ = dist_cart3S (X,Y,Z) iff for x1, y1 being Element of X
for x2, y2 being Element of Y
for x3, y3 being Element of Z
for x, y being Element of [: the carrier of X, the carrier of Y, the carrier of Z:] st x = [x1,x2,x3] & y = [y1,y2,y3] holds
b₄ . (x,y) = sqrt ((((dist (x1,y1)) ^2) + ((dist (x2,y2)) ^2)) + ((dist (x3,y3)) ^2)) );