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 ;
( z in D & S1[z,z1] & S1[z,z2] implies z1 = z2 )
assume
z in D
;
( 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])]
;
( 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])]
;
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;
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 ;
( z in D implies ex z1 being object st S1[z,z1] )
assume
z in D
;
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])]
;
S1[z,[(f . [x1,y1]),(g . [x8,y8])]]
thus
S1[
z,
[(f . [x1,y1]),(g . [x8,y8])]]
by A13;
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
; ( ( 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 ) )
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 ;
( 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;
( 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
;
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;
verum
end;
let x, y, x9, y9 be object ; ( [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 )
; 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; verum