let dist1, dist2 be Function of [: the carrier of X, the carrier of X:],REAL; :: thesis: ( ( for x, y being Point of X holds dist1 . (x,y) = ||.(x - y).|| ) & ( for x, y being Point of X holds dist2 . (x,y) = ||.(x - y).|| ) implies dist1 = dist2 )
assume that
A2: for x, y being Point of X holds dist1 . (x,y) = ||.(x - y).|| and
A3: for x, y being Point of X holds dist2 . (x,y) = ||.(x - y).|| ; :: thesis: dist1 = dist2

now :: thesis: for x, y being Point of X holds dist1 . (x,y) = dist2 . (x,y)

let x, y be Point of X; :: thesis: dist1 . (x,y) = dist2 . (x,y)
dist1 . (x,y) = ||.(x - y).|| by A2;
hence dist1 . (x,y) = dist2 . (x,y) by A3; :: thesis: verum

end;

hence dist1 = dist2 by BINOP_1:2; :: thesis: verum