set CX = the carrier of X;
deffunc H₁( Element of the carrier of X, Element of the carrier of X) -> Element of REAL = ||.($1 - $2).||;
ex f being Function of [: the carrier of X, the carrier of X:],REAL st
for x, y being Element of the carrier of X holds f . (x,y) = H₁(x,y) from BINOP_1:sch 4();
hence ex b₁ being Function of [: the carrier of X, the carrier of X:],REAL st
for x, y being Point of X holds b₁ . (x,y) = ||.(x - y).|| ; :: thesis: verum