defpred S₁[ set , set ] means ex x, y, x', y' being set st
( $1 = [[x,x'],[y,y']] & $2 = [(f . [x,y]),(g . [x',y'])] );
defpred S₂[ set ] means ex y being set st [$1,y] in dom f;
consider D1 being set such that
A1: for x being set holds
( x in D1 iff ( x in union (union (dom f)) & S₂[x] ) ) from XBOOLE_0:sch 1();
defpred S₃[ set ] means ex x being set st [x,$1] in dom f;
consider D2 being set such that
A2: for y being set holds
( y in D2 iff ( y in union (union (dom f)) & S₃[y] ) ) from XBOOLE_0:sch 1();
defpred S₄[ set ] means ex y being set st [$1,y] in dom g;
consider D1' being set such that
A3: for x being set holds
( x in D1' iff ( x in union (union (dom g)) & S₄[x] ) ) from XBOOLE_0:sch 1();
defpred S₅[ set ] means ex x being set st [x,$1] in dom g;
consider D2' being set such that
A4: for y being set holds
( y in D2' iff ( y in union (union (dom g)) & S₅[y] ) ) from XBOOLE_0:sch 1();
defpred S₆[ set ] means ex x, y, x', y' being set st
( $1 = [[x,x'],[y,y']] & [x,y] in dom f & [x',y'] in dom g );
consider D being set such that
A5: for z being set holds
( z in D iff ( z in [:[:D1,D1':],[:D2,D2':]:] & S₆[z] ) ) from XBOOLE_0:sch 1();
A6: for z, z1, z2 being set st z in D & S₁[z,z1] & S₁[z,z2] holds
z1 = z2

proof

let z, z1, z2 be set ; :: thesis: ( z in D & S₁[z,z1] & S₁[z,z2] implies z1 = z2 )
assume z in D ; :: thesis: ( not S₁[z,z1] or not S₁[z,z2] or z1 = z2 )
given x, y, x', y' being set such that A7: z = [[x,x'],[y,y']] and
A8: z1 = [(f . [x,y]),(g . [x',y'])] ; :: thesis: ( not S₁[z,z2] or z1 = z2 )
given x1, y1, x1', y1' being set such that A9: z = [[x1,x1'],[y1,y1']] and
A10: z2 = [(f . [x1,y1]),(g . [x1',y1'])] ; :: thesis: z1 = z2
A11: x' = x1' by A7, A9, Lm2;
( x = x1 & y = y1 ) by A7, A9, Lm2;
hence z1 = z2 by A7, A8, A9, A10, A11, Lm2; :: thesis: verum

end;

A12: for z being set st z in D holds
ex z1 being set st S₁[z,z1]

proof

let z be set ; :: thesis: ( z in D implies ex z1 being set st S₁[z,z1] )
assume z in D ; :: thesis: ex z1 being set st S₁[z,z1]
then consider x, y, x', y' being set such that
A13: z = [[x,x'],[y,y']] and
[x,y] in dom f and
[x',y'] in dom g by A5;
take [(f . [x,y]),(g . [x',y'])] ; :: thesis: S₁[z,[(f . [x,y]),(g . [x',y'])]]
thus S₁[z,[(f . [x,y]),(g . [x',y'])]] by A13; :: thesis: verum

end;

consider h being Function such that
A14: dom h = D and
A15: for z being set st z in D holds
S₁[z,h . z] from FUNCT_1:sch 2(A6, A12);
take h ; :: thesis: ( ( for z being set holds
( z in dom h iff ex x, y, x', y' being set st
( z = [[x,x'],[y,y']] & [x,y] in dom f & [x',y'] in dom g ) ) ) & ( for x, y, x', y' being set st [x,y] in dom f & [x',y'] in dom g holds
h . [x,x'],[y,y'] = [(f . x,y),(g . x',y')] ) )
thus A16: for z being set holds
( z in dom h iff ex x, y, x', y' being set st
( z = [[x,x'],[y,y']] & [x,y] in dom f & [x',y'] in dom g ) ) :: thesis: for x, y, x', y' being set st [x,y] in dom f & [x',y'] in dom g holds
h . [x,x'],[y,y'] = [(f . x,y),(g . x',y')]

proof

let z be set ; :: thesis: ( z in dom h iff ex x, y, x', y' being set st
( z = [[x,x'],[y,y']] & [x,y] in dom f & [x',y'] in dom g ) )
thus ( z in dom h implies ex x, y, x', y' being set st
( z = [[x,x'],[y,y']] & [x,y] in dom f & [x',y'] in dom g ) ) by A5, A14; :: thesis: ( ex x, y, x', y' being set st
( z = [[x,x'],[y,y']] & [x,y] in dom f & [x',y'] in dom g ) implies z in dom h )
given x, y, x', y' being set such that A17: z = [[x,x'],[y,y']] and
A18: [x,y] in dom f and
A19: [x',y'] in dom g ; :: thesis: z in dom h
y' in union (union (dom g)) by A19, Lm1;
then A20: y' in D2' by A4, A19;
y in union (union (dom f)) by A18, Lm1;
then y in D2 by A2, A18;
then A21: [y,y'] in [:D2,D2':] by A20, ZFMISC_1:106;
x' in union (union (dom g)) by A19, Lm1;
then A22: x' in D1' by A3, A19;
x in union (union (dom f)) by A18, Lm1;
then x in D1 by A1, A18;
then [x,x'] in [:D1,D1':] by A22, ZFMISC_1:106;
then z in [:[:D1,D1':],[:D2,D2':]:] by A17, A21, ZFMISC_1:106;
hence z in dom h by A5, A14, A17, A18, A19; :: thesis: verum

end;

let x, y, x', y' be set ; :: thesis: ( [x,y] in dom f & [x',y'] in dom g implies h . [x,x'],[y,y'] = [(f . x,y),(g . x',y')] )
assume ( [x,y] in dom f & [x',y'] in dom g ) ; :: thesis: h . [x,x'],[y,y'] = [(f . x,y),(g . x',y')]
then [[x,x'],[y,y']] in D by A14, A16;
then consider x1, y1, x1', y1' being set such that
A23: [[x,x'],[y,y']] = [[x1,x1'],[y1,y1']] and
A24: h . [[x,x'],[y,y']] = [(f . [x1,y1]),(g . [x1',y1'])] by A15;
A25: x' = x1' by A23, Lm2;
( x = x1 & y = y1 ) by A23, Lm2;
hence h . [x,x'],[y,y'] = [(f . x,y),(g . x',y')] by A23, A24, A25, Lm2; :: thesis: verum