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