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

proof

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

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

( dom f = [:X,Y:] & dom g = [:X',Y':] ) by A1, FUNCT_2:def 1;
hence [:[:X,X':],[:Y,Y':]:] = dom R by Th61; :: thesis: verum
thus verum ; :: thesis: verum

end;

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

hence R = {} ; :: thesis: verum

end;

end;

end;

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