:: deftheorem Def7 defines dist_cart4 METRIC_3:def 7 :
for X, Y, Z, W being non empty MetrSpace
for b₅ being Function of [:[: the carrier of X, the carrier of Y, the carrier of Z, the carrier of W:],[: the carrier of X, the carrier of Y, the carrier of Z, the carrier of W:]:],REAL holds
( b₅ = dist_cart4 (X,Y,Z,W) iff for x1, y1 being Element of X
for x2, y2 being Element of Y
for x3, y3 being Element of Z
for x4, y4 being Element of W
for x, y being Element of [: the carrier of X, the carrier of Y, the carrier of Z, the carrier of W:] st x = [x1,x2,x3,x4] & y = [y1,y2,y3,y4] holds
b₅ . (x,y) = ((dist (x1,y1)) + (dist (x2,y2))) + ((dist (x3,y3)) + (dist (x4,y4))) );