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