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