let X, Y, Z, X9, Y9, Z9 be set ; :: thesis: for f being Function of [:X,Y:],Z
for g being Function of [:X9,Y9:],Z9 st Z <> {} & Z9 <> {} holds
|:f,g:| is Function of [:[:X,X9:],[:Y,Y9:]:],[:Z,Z9:]
let f be Function of [:X,Y:],Z; :: thesis: for g being Function of [:X9,Y9:],Z9 st Z <> {} & Z9 <> {} holds
|:f,g:| is Function of [:[:X,X9:],[:Y,Y9:]:],[:Z,Z9:]
let g be Function of [:X9,Y9:],Z9; :: thesis: ( Z <> {} & Z9 <> {} implies |:f,g:| is Function of [:[:X,X9:],[:Y,Y9:]:],[:Z,Z9:] )
( rng |:f,g:| c= [:(rng f),(rng g):] & [:(rng f),(rng g):] c= [:Z,Z9:] ) by Th59, ZFMISC_1:96;
then A1: rng |:f,g:| c= [:Z,Z9:] by XBOOLE_1:1;
assume A2: ( Z <> {} & Z9 <> {} ) ; :: thesis: |:f,g:| is Function of [:[:X,X9:],[:Y,Y9:]:],[:Z,Z9:]
then ( dom f = [:X,Y:] & dom g = [:X9,Y9:] ) by FUNCT_2:def 1;
then [:[:X,X9:],[:Y,Y9:]:] = dom |:f,g:| by Th61;
then reconsider R = |:f,g:| as Relation of [:[:X,X9:],[:Y,Y9:]:],[:Z,Z9:] by A1, RELSET_1:4;
R is quasi_total

proof

per cases not ( [:Z,Z9:] = {} & not [:[:X,X9:],[:Y,Y9:]:] = {} & not ( [:Z,Z9:] = {} & [:[:X,X9:],[:Y,Y9:]:] <> {} ) ) ;
:: according to FUNCT_2:def 1

case ( [:Z,Z9:] = {} implies [:[:X,X9:],[:Y,Y9:]:] = {} ) ; :: thesis: [:[:X,X9:],[:Y,Y9:]:] = dom R

( dom f = [:X,Y:] & dom g = [:X9,Y9:] ) by A2, FUNCT_2:def 1;
hence [:[:X,X9:],[:Y,Y9:]:] = dom R by Th61; :: thesis: verum

end;

case ( [:Z,Z9:] = {} & [:[:X,X9:],[:Y,Y9:]:] <> {} ) ; :: thesis: R = {}

hence R = {} ; :: thesis: verum

end;

end;

end;

hence |:f,g:| is Function of [:[:X,X9:],[:Y,Y9:]:],[:Z,Z9:] ; :: thesis: verum