let X, Y, Z be set ; :: thesis: for f being Function of X,Y
for g being Function of X,Z st ( Y = {} implies X = {} ) & ( Z = {} implies X = {} ) holds
<:f,g:> is Function of X,[:Y,Z:]
let f be Function of X,Y; :: thesis: for g being Function of X,Z st ( Y = {} implies X = {} ) & ( Z = {} implies X = {} ) holds
<:f,g:> is Function of X,[:Y,Z:]
let g be Function of X,Z; :: thesis: ( ( Y = {} implies X = {} ) & ( Z = {} implies X = {} ) implies <:f,g:> is Function of X,[:Y,Z:] )
assume A1: ( ( Y = {} implies X = {} ) & ( Z = {} implies X = {} ) ) ; :: thesis: <:f,g:> is Function of X,[:Y,Z:]

per cases not ( [:Y,Z:] = {} & not X = {} & not ( [:Y,Z:] = {} & X <> {} ) ) ;

suppose A2: ( [:Y,Z:] = {} implies X = {} ) ; :: thesis: <:f,g:> is Function of X,[:Y,Z:]

( rng f c= Y & rng g c= Z ) by RELAT_1:def 19;
then ( [:(rng f),(rng g):] c= [:Y,Z:] & rng <:f,g:> c= [:(rng f),(rng g):] & dom f = X & dom g = X ) by A1, Th71, FUNCT_2:def 1, ZFMISC_1:119;
then ( dom <:f,g:> = X & rng <:f,g:> c= [:Y,Z:] ) by Th70, XBOOLE_1:1;
hence <:f,g:> is Function of X,[:Y,Z:] by A2, FUNCT_2:def 1, RELSET_1:11; :: thesis: verum

end;

suppose ( [:Y,Z:] = {} & X <> {} ) ; :: thesis: <:f,g:> is Function of X,[:Y,Z:]

hence <:f,g:> is Function of X,[:Y,Z:] by A1; :: thesis: verum

end;

end;