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