deffunc H1( Point of (TOP-REAL n), Point of (TOP-REAL n)) -> object = |.($1 - $2).|;
A2:
for p, q being Point of (TOP-REAL n) holds H1(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) = H1(p,q)
from FUNCT_7:sch 1(A2);
reconsider f = f as RealMap of [:(TOP-REAL n),(TOP-REAL n):] by A1;
take
f
; for p, q being Point of (TOP-REAL n) holds f . (p,q) = |.(p - q).|
let p, q be Point of (TOP-REAL n); f . (p,q) = |.(p - q).|
thus
f . (p,q) = |.(p - q).|
by A3; verum