let X, Y, Z, X', Y', Z' be set ; :: thesis: for f being PartFunc of ,
for g being PartFunc of , holds |:f,g:| is PartFunc of ,
let f be PartFunc of ,; :: thesis: for g being PartFunc of , holds |:f,g:| is PartFunc of ,
let g be PartFunc of ,; :: thesis: |:f,g:| is PartFunc of ,
( rng |:f,g:| c= [:(rng f),(rng g):] & [:(rng f),(rng g):] c= [:Z,Z':] ) by Th59, ZFMISC_1:119;
then A1: rng |:f,g:| c= [:Z,Z':] by XBOOLE_1:1;
( dom f c= [:X,Y:] & dom g c= [:X',Y':] ) ;
then dom |:f,g:| c= [:[:X,X':],[:Y,Y':]:] by Th60;
hence |:f,g:| is PartFunc of , by A1, RELSET_1:11; :: thesis: verum