set CX = the carrier of X;
deffunc H₁( Element of the carrier of X, Element of the carrier of X) -> Element of REAL = In (||.($1 - $2).||,REAL);
consider f being Function of [: the carrier of X, the carrier of X:],REAL such that
A1: for x, y being Element of the carrier of X holds f . (x,y) = H₁(x,y) from BINOP_1:sch 4();
take f ; :: thesis: for x, y being Point of X holds f . (x,y) = ||.(x - y).||
let x, y be Point of X; :: thesis: f . (x,y) = ||.(x - y).||
f . (x,y) = H₁(x,y) by A1;
hence f . (x,y) = ||.(x - y).|| ; :: thesis: verum