for M, N being MetrStruct
for x, y being Element of M
for a, b being Element of N st MetrStruct(# the carrier of M, the distance of M #) = MetrStruct(# the carrier of N, the distance of N #) & x = a & y = b holds
dist (x,y) = dist (a,b) ;