let X, X9, Y, Y9 be set ; 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; ( 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:] )
; dom |:f,g:| = [:[:X,X9:],[:Y,Y9:]:]
hence
dom |:f,g:| c= [:[:X,X9:],[:Y,Y9:]:]
by Th57; XBOOLE_0:def 10 [:[:X,X9:],[:Y,Y9:]:] c= dom |:f,g:|
let z be object ; TARSKI:def 3 ( not z in [:[:X,X9:],[:Y,Y9:]:] or z in dom |:f,g:| )
assume
z in [:[:X,X9:],[:Y,Y9:]:]
; 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; verum