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