let X, X9, Y, Y9, Z, 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 Th56, ZFMISC_1:96;
then A1: rng |:f,g:| c= [:Z,Z9:] ;
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 Th58;
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 ( [:Z,Z9:] <> {} or [:Z,Z9:] = {} ) ;
:: according to FUNCT_2:def 1

case [:Z,Z9:] <> {} ; :: 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 Th58; :: thesis: verum

end;

case [:Z,Z9:] = {} ; :: thesis: R = {}

hence R = {} ; :: thesis: verum

end;

end;

end;

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