reconsider h = <:f,g:> as X /\ Y -defined Function ;
( dom f = X & dom g = Y ) by PARTFUN1:def 2;
then dom h = X /\ Y by FUNCT_3:def 7;
hence for b₁ being X /\ Y -defined Function st b₁ = <:f,g:> holds
b₁ is total by PARTFUN1:def 2; :: thesis: verum