let X, Y, Z, X9, Y9, Z9 be set ; :: thesis: for f being PartFunc of [:X,Y:],Z
for g being PartFunc of [:X9,Y9:],Z9 holds |:f,g:| is PartFunc of [:[:X,X9:],[:Y,Y9:]:],[:Z,Z9:]
let f be PartFunc of [:X,Y:],Z; :: thesis: for g being PartFunc of [:X9,Y9:],Z9 holds |:f,g:| is PartFunc of [:[:X,X9:],[:Y,Y9:]:],[:Z,Z9:]
let g be PartFunc of [:X9,Y9:],Z9; :: thesis: |:f,g:| is PartFunc 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:119;
then A1: rng |:f,g:| c= [:Z,Z9:] by XBOOLE_1:1;
( dom f c= [:X,Y:] & dom g c= [:X9,Y9:] ) ;
then dom |:f,g:| c= [:[:X,X9:],[:Y,Y9:]:] by Th60;
hence |:f,g:| is PartFunc of [:[:X,X9:],[:Y,Y9:]:],[:Z,Z9:] by A1, RELSET_1:11; :: thesis: verum