deffunc H₁( Point of (TOP-REAL n), Point of (TOP-REAL n)) -> Element of REAL = |.($1 - $2).|;
A2: for p, q being Point of (TOP-REAL n) holds H₁(p,q) in REAL ;
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