deffunc H₁( set , set ) -> set = $1;
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 = x ) ) ; :: thesis: verum