:: deftheorem Def10 defines dist_cart2S METRIC_3:def 10 :
for X, Y being non empty MetrSpace
for b₃ being Function of [:[: the carrier of X, the carrier of Y:],[: the carrier of X, the carrier of Y:]:],REAL holds
( b₃ = dist_cart2S (X,Y) iff for x1, y1 being Element of X
for x2, y2 being Element of Y
for x, y being Element of [: the carrier of X, the carrier of Y:] st x = [x1,x2] & y = [y1,y2] holds
b₃ . (x,y) = sqrt (((dist (x1,y1)) ^2) + ((dist (x2,y2)) ^2)) );