defpred S1[ object , object ] means for x1, y1 being object st $1 = [x1,y1] holds
P1[x1,y1,$2];
A3:
for x, z being object st x in [:F1(),F2():] & S1[x,z] holds
z in F3()
proof
let x,
z be
object ;
( x in [:F1(),F2():] & S1[x,z] implies z in F3() )
assume
x in [:F1(),F2():]
;
( not S1[x,z] or z in F3() )
then A4:
ex
x1,
y1 being
object st
(
x1 in F1() &
y1 in F2() &
x = [x1,y1] )
by ZFMISC_1:def 2;
assume
for
x1,
y1 being
object st
x = [x1,y1] holds
P1[
x1,
y1,
z]
;
z in F3()
hence
z in F3()
by A1, A4;
verum
end;
A5:
for x, z1, z2 being object st x in [:F1(),F2():] & S1[x,z1] & S1[x,z2] holds
z1 = z2
proof
let x,
z1,
z2 be
object ;
( x in [:F1(),F2():] & S1[x,z1] & S1[x,z2] implies z1 = z2 )
assume that A6:
x in [:F1(),F2():]
and A7:
( ( for
x1,
y1 being
object st
x = [x1,y1] holds
P1[
x1,
y1,
z1] ) & ( for
x1,
y1 being
object st
x = [x1,y1] holds
P1[
x1,
y1,
z2] ) )
;
z1 = z2
consider x1,
y1 being
object such that A8:
(
x1 in F1() &
y1 in F2() )
and A9:
x = [x1,y1]
by A6, ZFMISC_1:def 2;
(
P1[
x1,
y1,
z1] &
P1[
x1,
y1,
z2] )
by A7, A9;
hence
z1 = z2
by A2, A8;
verum
end;
consider f being PartFunc of [:F1(),F2():],F3() such that
A10:
for x being object holds
( x in dom f iff ( x in [:F1(),F2():] & ex z being object st S1[x,z] ) )
and
A11:
for x being object st x in dom f holds
S1[x,f . x]
from PARTFUN1:sch 2(A3, A5);
take
f
; ( ( for x, y being object holds
( [x,y] in dom f iff ( x in F1() & y in F2() & ex z being object st P1[x,y,z] ) ) ) & ( for x, y being object st [x,y] in dom f holds
P1[x,y,f . (x,y)] ) )
thus
for x, y being object holds
( [x,y] in dom f iff ( x in F1() & y in F2() & ex z being object st P1[x,y,z] ) )
for x, y being object st [x,y] in dom f holds
P1[x,y,f . (x,y)]proof
let x,
y be
object ;
( [x,y] in dom f iff ( x in F1() & y in F2() & ex z being object st P1[x,y,z] ) )
thus
(
[x,y] in dom f implies (
x in F1() &
y in F2() & ex
z being
object st
P1[
x,
y,
z] ) )
( x in F1() & y in F2() & ex z being object st P1[x,y,z] implies [x,y] in dom f )proof
assume A12:
[x,y] in dom f
;
( x in F1() & y in F2() & ex z being object st P1[x,y,z] )
hence
(
x in F1() &
y in F2() )
by ZFMISC_1:87;
ex z being object st P1[x,y,z]
consider z being
object such that A13:
for
x1,
y1 being
object st
[x,y] = [x1,y1] holds
P1[
x1,
y1,
z]
by A10, A12;
take
z
;
P1[x,y,z]
thus
P1[
x,
y,
z]
by A13;
verum
end;
assume
(
x in F1() &
y in F2() )
;
( for z being object holds P1[x,y,z] or [x,y] in dom f )
then A14:
[x,y] in [:F1(),F2():]
by ZFMISC_1:def 2;
given z being
object such that A15:
P1[
x,
y,
z]
;
[x,y] in dom f
now ex z being object st
for x1, y1 being object st [x,y] = [x1,y1] holds
P1[x1,y1,z]take z =
z;
for x1, y1 being object st [x,y] = [x1,y1] holds
P1[x1,y1,z]let x1,
y1 be
object ;
( [x,y] = [x1,y1] implies P1[x1,y1,z] )assume A16:
[x,y] = [x1,y1]
;
P1[x1,y1,z]then
x = x1
by XTUPLE_0:1;
hence
P1[
x1,
y1,
z]
by A15, A16, XTUPLE_0:1;
verum end;
hence
[x,y] in dom f
by A10, A14;
verum
end;
thus
for x, y being object st [x,y] in dom f holds
P1[x,y,f . (x,y)]
by A11; verum