deffunc H_{1}( Element of the carrier of X) -> object = ||.$1.||;

X0: for x being Element of the carrier of X holds H_{1}(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_{1}(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

X0: for x being Element of the carrier of X holds H

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

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