deffunc H₁( Point of ) -> Point of = FanW s,$1;
thus for f, g being Function of (TOP-REAL 2),(TOP-REAL 2) st ( for q being Point of holds f . q = H₁(q) ) & ( for q being Point of holds g . q = H₁(q) ) holds
f = g from BINOP_2:sch 1(); :: thesis: verum