let X, X9, Y, Y9, Z, 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 Th56, ZFMISC_1:96;
then A1: rng |:f,g:| c= [:Z,Z9:] ;
( dom f c= [:X,Y:] & dom g c= [:X9,Y9:] ) ;
then dom |:f,g:| c= [:[:X,X9:],[:Y,Y9:]:] by Th57;
hence |:f,g:| is PartFunc of [:[:X,X9:],[:Y,Y9:]:],[:Z,Z9:] by A1, RELSET_1:4; :: thesis: verum