let X, X9, Y, Y9, Z, Z9 be set ; 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; 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; ( 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 <> {} )
; |: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
hence
|:f,g:| is Function of [:[:X,X9:],[:Y,Y9:]:],[:Z,Z9:]
; verum