( rng f c= X & rng g c= Y ) by RELAT_1:def 19;
then B0: [:(rng f),(rng g):] c= [:X,Y:] by ZFMISC_1:96;
set h = <:f,g:>;
rng <:f,g:> c= [:(rng f),(rng g):] by FUNCT_3:51;
then rng <:f,g:> c= [:X,Y:] by B0, XBOOLE_1:1;
hence for b₁ being Function st b₁ = <:f,g:> holds
b₁ is [:X,Y:] -valued by RELAT_1:def 19; :: thesis: verum