deffunc H₁( Point of (TOP-REAL n)) -> Element of REAL = |.$1.|;
A1: for x being Element of (TOP-REAL n) holds H₁(x) in the carrier of R^1 by TOPMETR:24;
thus ex IT being Function of (TOP-REAL n),R^1 st
for q being Point of (TOP-REAL n) holds IT . q = H₁(q) from FUNCT_2:sch 8(A1); :: thesis: verum