reconsider F = dom f as Subset of X ;
reconsider G = dom g as Subset of Y ;
set h = <:f,g:>;
A1: dom <:f,g:> = G /\ F by FUNCT_3:def 7;
thus for b₁ being Function st b₁ = <:f,g:> holds
b₁ is X /\ Y -defined by XBOOLE_1:27, A1; :: thesis: verum