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