deffunc H₁( set , set ) -> set = $2;
ex f being Function st
( dom f = [:X,Y:] & ( for x, y being set st x in X & y in Y holds
f . (x,y) = H₁(x,y) ) ) from FUNCT_3:sch 2();
hence ex b₁ being Function st
( dom b₁ = [:X,Y:] & ( for x, y being set st x in X & y in Y holds
b₁ . (x,y) = y ) ) ; :: thesis: verum