thus for f, g being Function of [:I[01],I[01]:],T st ( for a, b being Point of I[01] holds f . (a,b) = H₁(a,b) ) & ( for a, b being Point of I[01] holds g . (a,b) = H₁(a,b) ) holds
f = g from TOPALG_7:sch 2(); :: thesis: verum