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