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