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