deffunc H₁( Point of ) -> Point of = FanN c,$1;
thus ex IT being Function of (TOP-REAL 2),(TOP-REAL 2) st
for q being Point of holds IT . q = H₁(q) from FUNCT_2:sch 4(); :: thesis: verum