defpred S1[ object , object ] means ex x, y, x9, y9 being object st
( $1 = [[x,x9],[y,y9]] & $2 = [(f . [x,y]),(g . [x9,y9])] );
defpred S2[ object ] means ex y being object st [$1,y] in dom f;
consider D1 being set such that
A1: for x being object holds
( x in D1 iff ( x in union (union (dom f)) & S2[x] ) ) from XBOOLE_0:sch 1();
 defpred S3[ object ] means ex x being object st [x,$1] in dom f;
consider D2 being set such that
A2: for y being object holds
( y in D2 iff ( y in union (union (dom f)) & S3[y] ) ) from XBOOLE_0:sch 1();
 defpred S4[ object ] means ex y being object st [$1,y] in dom g;
consider D19 being set such that
A3: for x being object holds
( x in D19 iff ( x in union (union (dom g)) & S4[x] ) ) from XBOOLE_0:sch 1();
 defpred S5[ object ] means ex x being object st [x,$1] in dom g;
consider D29 being set such that
A4: for y being object holds
( y in D29 iff ( y in union (union (dom g)) & S5[y] ) ) from XBOOLE_0:sch 1();
 defpred S6[ object ] means ex x, y, x9, y9 being object st
( $1 = [[x,x9],[y,y9]] & [x,y] in dom f & [x9,y9] in dom g );
consider D being set such that
A5: for z being object holds
( z in D iff ( z in [:[:D1,D19:],[:D2,D29:]:] & S6[z] ) ) from XBOOLE_0:sch 1();
 A6: for z, z1, z2 being object st z in D & S1[z,z1] & S1[z,z2] holds
z1 = z2
proof
let z, z1, z2 be object ; :: thesis: ( z in D & S1[z,z1] & S1[z,z2] implies z1 = z2 )
assume z in D ; :: thesis: ( not S1[z,z1] or not S1[z,z2] or z1 = z2 )
given x, y, x9, y9 being object such that A7: z = [[x,x9],[y,y9]] and
A8: z1 = [(f . [x,y]),(g . [x9,y9])] ; :: thesis: ( not S1[z,z2] or z1 = z2 )
given x1, y1, x19, y19 being object such that A9: z = [[x1,x19],[y1,y19]] and
A10: z2 = [(f . [x1,y1]),(g . [x19,y19])] ; :: thesis: z1 = z2
A11: x9 = x19 by A7, A9, Lm1;
( x = x1 & y = y1 ) by A7, A9, Lm1;
hence z1 = z2 by A7, A8, A9, A10, A11, Lm1; :: thesis: verum
end;
A12: for z being object st z in D holds
ex z1 being object st S1[z,z1]
proof
let z be object ; :: thesis: ( z in D implies ex z1 being object st S1[z,z1] )
assume z in D ; :: thesis: ex z1 being object st S1[z,z1]
then consider x1, y1, x8, y8 being object such that
A13: z = [[x1,x8],[y1,y8]] and
[x1,y1] in dom f and
[x8,y8] in dom g by A5;
take [(f . [x1,y1]),(g . [x8,y8])] ; :: thesis: S1[z,[(f . [x1,y1]),(g . [x8,y8])]]
thus S1[z,[(f . [x1,y1]),(g . [x8,y8])]] by A13; :: thesis: verum
end;
consider h being Function such that
A14: dom h = D and
A15: for z being object st z in D holds
S1[z,h . z] from FUNCT_1:sch 2(A6, A12);
 take h ; :: thesis: ( ( for z being object holds
( z in dom h iff ex x, y, x9, y9 being object st
( z = [[x,x9],[y,y9]] & [x,y] in dom f & [x9,y9] in dom g ) ) ) & ( for x, y, x9, y9 being object st [x,y] in dom f & [x9,y9] in dom g holds
h . ([x,x9],[y,y9]) = [(f . (x,y)),(g . (x9,y9))] ) )
thus A16: for z being object holds
( z in dom h iff ex x, y, x9, y9 being object st
( z = [[x,x9],[y,y9]] & [x,y] in dom f & [x9,y9] in dom g ) ) :: thesis: for x, y, x9, y9 being object st [x,y] in dom f & [x9,y9] in dom g holds
h . ([x,x9],[y,y9]) = [(f . (x,y)),(g . (x9,y9))]
proof
let z be object ; :: thesis: ( z in dom h iff ex x, y, x9, y9 being object st
( z = [[x,x9],[y,y9]] & [x,y] in dom f & [x9,y9] in dom g ) )
thus ( z in dom h implies ex x, y, x9, y9 being object st
( z = [[x,x9],[y,y9]] & [x,y] in dom f & [x9,y9] in dom g ) ) by A5, A14; :: thesis: ( ex x, y, x9, y9 being object st
( z = [[x,x9],[y,y9]] & [x,y] in dom f & [x9,y9] in dom g ) implies z in dom h )
given x, y, x9, y9 being object such that A17: z = [[x,x9],[y,y9]] and
A18: [x,y] in dom f and
A19: [x9,y9] in dom g ; :: thesis: z in dom h
y9 in union (union (dom g)) by A19, ZFMISC_1:134;
then A20: y9 in D29 by A4, A19;
y in union (union (dom f)) by A18, ZFMISC_1:134;
then y in D2 by A2, A18;
then A21: [y,y9] in [:D2,D29:] by A20, ZFMISC_1:87;
x9 in union (union (dom g)) by A19, ZFMISC_1:134;
then A22: x9 in D19 by A3, A19;
x in union (union (dom f)) by A18, ZFMISC_1:134;
then x in D1 by A1, A18;
then [x,x9] in [:D1,D19:] by A22, ZFMISC_1:87;
then z in [:[:D1,D19:],[:D2,D29:]:] by A17, A21, ZFMISC_1:87;
hence z in dom h by A5, A14, A17, A18, A19; :: thesis: verum
end;
let x, y, x9, y9 be object ; :: thesis: ( [x,y] in dom f & [x9,y9] in dom g implies h . ([x,x9],[y,y9]) = [(f . (x,y)),(g . (x9,y9))] )
assume ( [x,y] in dom f & [x9,y9] in dom g ) ; :: thesis: h . ([x,x9],[y,y9]) = [(f . (x,y)),(g . (x9,y9))]
then [[x,x9],[y,y9]] in D by A14, A16;
then consider x1, y1, x19, y19 being object such that
A23: [[x,x9],[y,y9]] = [[x1,x19],[y1,y19]] and
A24: h . [[x,x9],[y,y9]] = [(f . [x1,y1]),(g . [x19,y19])] by A15;
A25: x9 = x19 by A23, Lm1;
( x = x1 & y = y1 ) by A23, Lm1;
hence h . ([x,x9],[y,y9]) = [(f . (x,y)),(g . (x9,y9))] by A23, A24, A25, Lm1; :: thesis: verum