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