deffunc H₁( Element of the carrier of X) -> object = ||.$1.||;
X0: for x being Element of the carrier of X holds H₁(x) in REAL by XREAL_0:def 1;
consider f being Function of the carrier of X,REAL such that
X1: for x being Element of the carrier of X holds f . x = H₁(x) from FUNCT_2:sch 8(X0);
take f ; :: thesis: for x being Point of X holds f . x = ||.x.||
thus for x being Point of X holds f . x = ||.x.|| by X1; :: thesis: verum