thus for f, g being Function of (TOP-REAL n),R^1 st ( for q being Point of (TOP-REAL n) holds f . q = H₁(q) ) & ( for q being Point of (TOP-REAL n) holds g . q = H₁(q) ) holds
f = g from BINOP_2:sch 1(); :: thesis: verum