deffunc H₁( Point of , Point of ) -> Element of REAL = |.($1 - $2).|;
A2: for p, q being Point of 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 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 holds f . p,q = |.(p - q).|
let p, q be Point of ; :: thesis: f . p,q = |.(p - q).|
thus f . p,q = |.(p - q).| by A3; :: thesis: verum