defpred S_{1}[ object , object ] means for x1, y1 being object st $1 = [x1,y1] holds

P_{1}[x1,y1,$2];

A3: for x, z being object st x in [:F_{1}(),F_{2}():] & S_{1}[x,z] holds

z in F_{3}()
_{1}(),F_{2}():] & S_{1}[x,z1] & S_{1}[x,z2] holds

z1 = z2_{1}(),F_{2}():],F_{3}() such that

A10: for x being object holds

( x in dom f iff ( x in [:F_{1}(),F_{2}():] & ex z being object st S_{1}[x,z] ) )
and

A11: for x being object st x in dom f holds

S_{1}[x,f . x]
from PARTFUN1:sch 2(A3, A5);

take f ; :: thesis: ( ( for x, y being object holds

( [x,y] in dom f iff ( x in F_{1}() & y in F_{2}() & ex z being object st P_{1}[x,y,z] ) ) ) & ( for x, y being object st [x,y] in dom f holds

P_{1}[x,y,f . (x,y)] ) )

thus for x, y being object holds

( [x,y] in dom f iff ( x in F_{1}() & y in F_{2}() & ex z being object st P_{1}[x,y,z] ) )
:: thesis: for x, y being object st [x,y] in dom f holds

P_{1}[x,y,f . (x,y)]

P_{1}[x,y,f . (x,y)]
by A11; :: thesis: verum

P

A3: for x, z being object st x in [:F

z in F

proof

A5:
for x, z1, z2 being object st x in [:F
let x, z be object ; :: thesis: ( x in [:F_{1}(),F_{2}():] & S_{1}[x,z] implies z in F_{3}() )

assume x in [:F_{1}(),F_{2}():]
; :: thesis: ( not S_{1}[x,z] or z in F_{3}() )

then A4: ex x1, y1 being object st

( x1 in F_{1}() & y1 in F_{2}() & x = [x1,y1] )
by ZFMISC_1:def 2;

assume for x1, y1 being object st x = [x1,y1] holds

P_{1}[x1,y1,z]
; :: thesis: z in F_{3}()

hence z in F_{3}()
by A1, A4; :: thesis: verum

end;assume x in [:F

then A4: ex x1, y1 being object st

( x1 in F

assume for x1, y1 being object st x = [x1,y1] holds

P

hence z in F

z1 = z2

proof

consider f being PartFunc of [:F
let x, z1, z2 be object ; :: thesis: ( x in [:F_{1}(),F_{2}():] & S_{1}[x,z1] & S_{1}[x,z2] implies z1 = z2 )

assume that

A6: x in [:F_{1}(),F_{2}():]
and

A7: ( ( for x1, y1 being object st x = [x1,y1] holds

P_{1}[x1,y1,z1] ) & ( for x1, y1 being object st x = [x1,y1] holds

P_{1}[x1,y1,z2] ) )
; :: thesis: z1 = z2

consider x1, y1 being object such that

A8: ( x1 in F_{1}() & y1 in F_{2}() )
and

A9: x = [x1,y1] by A6, ZFMISC_1:def 2;

( P_{1}[x1,y1,z1] & P_{1}[x1,y1,z2] )
by A7, A9;

hence z1 = z2 by A2, A8; :: thesis: verum

end;assume that

A6: x in [:F

A7: ( ( for x1, y1 being object st x = [x1,y1] holds

P

P

consider x1, y1 being object such that

A8: ( x1 in F

A9: x = [x1,y1] by A6, ZFMISC_1:def 2;

( P

hence z1 = z2 by A2, A8; :: thesis: verum

A10: for x being object holds

( x in dom f iff ( x in [:F

A11: for x being object st x in dom f holds

S

take f ; :: thesis: ( ( for x, y being object holds

( [x,y] in dom f iff ( x in F

P

thus for x, y being object holds

( [x,y] in dom f iff ( x in F

P

proof

thus
for x, y being object st [x,y] in dom f holds
let x, y be object ; :: thesis: ( [x,y] in dom f iff ( x in F_{1}() & y in F_{2}() & ex z being object st P_{1}[x,y,z] ) )

thus ( [x,y] in dom f implies ( x in F_{1}() & y in F_{2}() & ex z being object st P_{1}[x,y,z] ) )
:: thesis: ( x in F_{1}() & y in F_{2}() & ex z being object st P_{1}[x,y,z] implies [x,y] in dom f )_{1}() & y in F_{2}() )
; :: thesis: ( for z being object holds P_{1}[x,y,z] or [x,y] in dom f )

then A14: [x,y] in [:F_{1}(),F_{2}():]
by ZFMISC_1:def 2;

given z being object such that A15: P_{1}[x,y,z]
; :: thesis: [x,y] in dom f

end;thus ( [x,y] in dom f implies ( x in F

proof

assume
( x in F
assume A12:
[x,y] in dom f
; :: thesis: ( x in F_{1}() & y in F_{2}() & ex z being object st P_{1}[x,y,z] )

hence ( x in F_{1}() & y in F_{2}() )
by ZFMISC_1:87; :: thesis: ex z being object st P_{1}[x,y,z]

consider z being object such that

A13: for x1, y1 being object st [x,y] = [x1,y1] holds

P_{1}[x1,y1,z]
by A10, A12;

take z ; :: thesis: P_{1}[x,y,z]

thus P_{1}[x,y,z]
by A13; :: thesis: verum

end;hence ( x in F

consider z being object such that

A13: for x1, y1 being object st [x,y] = [x1,y1] holds

P

take z ; :: thesis: P

thus P

then A14: [x,y] in [:F

given z being object such that A15: P

now :: thesis: ex z being object st

for x1, y1 being object st [x,y] = [x1,y1] holds

P_{1}[x1,y1,z]

hence
[x,y] in dom f
by A10, A14; :: thesis: verumfor x1, y1 being object st [x,y] = [x1,y1] holds

P

take z = z; :: thesis: for x1, y1 being object st [x,y] = [x1,y1] holds

P_{1}[x1,y1,z]

let x1, y1 be object ; :: thesis: ( [x,y] = [x1,y1] implies P_{1}[x1,y1,z] )

assume A16: [x,y] = [x1,y1] ; :: thesis: P_{1}[x1,y1,z]

then x = x1 by XTUPLE_0:1;

hence P_{1}[x1,y1,z]
by A15, A16, XTUPLE_0:1; :: thesis: verum

end;P

let x1, y1 be object ; :: thesis: ( [x,y] = [x1,y1] implies P

assume A16: [x,y] = [x1,y1] ; :: thesis: P

then x = x1 by XTUPLE_0:1;

hence P

P