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
A1: for x, y being Point of X holds dist1 . x,y = ||.(x - y).|| and
A2: for x, y being Point of X holds dist2 . x,y = ||.(x - y).|| ; :: thesis: dist1 = dist2

now

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

end;

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