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