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