let X, X9, Y, Y9 be set ; :: thesis: for f, g being Function st dom f c= [:X,Y:] & dom g c= [:X9,Y9:] holds
dom |:f,g:| c= [:[:X,X9:],[:Y,Y9:]:]
let f, g be Function; :: thesis: ( dom f c= [:X,Y:] & dom g c= [:X9,Y9:] implies dom |:f,g:| c= [:[:X,X9:],[:Y,Y9:]:] )
assume A1: ( dom f c= [:X,Y:] & dom g c= [:X9,Y9:] ) ; :: thesis: dom |:f,g:| c= [:[:X,X9:],[:Y,Y9:]:]
let xy be object ; :: according to TARSKI:def 3 :: thesis: ( not xy in dom |:f,g:| or xy in [:[:X,X9:],[:Y,Y9:]:] )
assume xy in dom |:f,g:| ; :: thesis: xy in [:[:X,X9:],[:Y,Y9:]:]
then consider x, y, x9, y9 being object such that
A2: xy = [[x,x9],[y,y9]] and
A3: ( [x,y] in dom f & [x9,y9] in dom g ) by Def3;
( y in Y & y9 in Y9 ) by A1, A3, ZFMISC_1:87;
then A4: [y,y9] in [:Y,Y9:] by ZFMISC_1:87;
( x in X & x9 in X9 ) by A1, A3, ZFMISC_1:87;
then [x,x9] in [:X,X9:] by ZFMISC_1:87;
hence xy in [:[:X,X9:],[:Y,Y9:]:] by A2, A4, ZFMISC_1:87; :: thesis: verum