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();
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'])] );
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
( x = x1 & y = y1 & x' = x1' & y' = y1' ) by A7, A9, Lm2;
hence z1 = z2 by A8, A10; :: thesis: verum

end;

A11: 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
A12: z = [[x,x'],[y,y']] and
( [x,y] in dom f & [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 A12; :: thesis: verum

end;

consider h being Function such that
A13: dom h = D and
A14: for z being set st z in D holds
S₆[z,h . z] from FUNCT_1:sch 2(A6, A11);
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 A15: 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, A13; :: 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 A16: z = [[x,x'],[y,y']] and
A17: [x,y] in dom f and
A18: [x',y'] in dom g ; :: thesis: z in dom h
( x in union (union (dom f)) & y in union (union (dom f)) & x' in union (union (dom g)) & y' in union (union (dom g)) ) by A17, A18, Lm1;
then ( x in D1 & y in D2 & x' in D1' & y' in D2' ) by A1, A2, A3, A4, A17, A18;
then ( [x,x'] in [:D1,D1':] & [y,y'] in [:D2,D2':] ) by ZFMISC_1:106;
then z in [:[:D1,D1':],[:D2,D2':]:] by A16, ZFMISC_1:106;
hence z in dom h by A5, A13, A16, A17, A18; :: 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 that
A19: [x,y] in dom f and
A20: [x',y'] in dom g ; :: thesis: h . [x,x'],[y,y'] = [(f . x,y),(g . x',y')]
[[x,x'],[y,y']] in D by A13, A15, A19, A20;
then consider x1, y1, x1', y1' being set such that
A21: [[x,x'],[y,y']] = [[x1,x1'],[y1,y1']] and
A22: h . [[x,x'],[y,y']] = [(f . [x1,y1]),(g . [x1',y1'])] by A14;
( x = x1 & y = y1 & x' = x1' & y' = y1' ) by A21, Lm2;
hence h . [x,x'],[y,y'] = [(f . x,y),(g . x',y')] by A22; :: thesis: verum