deffunc H₁( Point of (TOP-REAL 2)) -> Element of REAL = $1 `2 ;
thus ex f being RealMap of (TOP-REAL 2) st
for p being Point of (TOP-REAL 2) holds f . p = H₁(p) from FUNCT_2:sch 4(); :: thesis: verum