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

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)

hence
dist1 = dist2
by BINOP_1:2; :: thesis: verumlet 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;dist1 . (x,y) = ||.(x - y).|| by A2;

hence dist1 . (x,y) = dist2 . (x,y) by A3; :: thesis: verum