A1: for x being Element of (TOP-REAL n) holds H₁(x) in the carrier of R^1 by TOPMETR:17, XREAL_0:def 1;
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