deffunc H₁( Point of (TOP-REAL n), Point of (TOP-REAL n)) -> object = |.($1 - $2).|;
A2: for p, q being Point of (TOP-REAL n) holds H₁(p,q) in REAL by XREAL_0:def 1;
consider f being Function of [: the carrier of (TOP-REAL n), the carrier of (TOP-REAL n):],REAL such that
A3: for p, q being Point of (TOP-REAL n) holds f . (p,q) = H₁(p,q) from FUNCT_7:sch 1(A2);
reconsider f = f as RealMap of [:(TOP-REAL n),(TOP-REAL n):] by A1;
take f ; :: thesis: for p, q being Point of (TOP-REAL n) holds f . (p,q) = |.(p - q).|
let p, q be Point of (TOP-REAL n); :: thesis: f . (p,q) = |.(p - q).|
thus f . (p,q) = |.(p - q).| by A3; :: thesis: verum