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

( ( P_{1}[x,y] implies $2 = F_{4}(x,y) ) & ( P_{2}[x,y] implies $2 = F_{5}(x,y) ) );

defpred S_{2}[ object ] means for x, y being object holds

( not $1 = [x,y] or P_{1}[x,y] or P_{2}[x,y] );

consider K being set such that

A4: for z being object holds

( z in K iff ( z in [:F_{1}(),F_{2}():] & S_{2}[z] ) )
from XBOOLE_0:sch 1();

A5: for x1 being object st x1 in K holds

ex z being object st S_{1}[x1,z]

A11: ( dom f = K & ( for z being object st z in K holds

S_{1}[z,f . z] ) )
from CLASSES1:sch 1(A5);

A12: rng f c= F_{3}()
_{1}(),F_{2}():]
by A4;

then reconsider f = f as PartFunc of [:F_{1}(),F_{2}():],F_{3}() by A11, A12, RELSET_1:4;

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

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

( ( P_{1}[x,y] implies f . [x,y] = F_{4}(x,y) ) & ( P_{2}[x,y] implies f . [x,y] = F_{5}(x,y) ) ) ) )

thus for x, y being object holds

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

( ( P_{1}[x,y] implies f . [x,y] = F_{4}(x,y) ) & ( P_{2}[x,y] implies f . [x,y] = F_{5}(x,y) ) )_{1}[x,y] implies f . [x,y] = F_{4}(x,y) ) & ( P_{2}[x,y] implies f . [x,y] = F_{5}(x,y) ) ) )

assume [x,y] in dom f ; :: thesis: ( ( P_{1}[x,y] implies f . [x,y] = F_{4}(x,y) ) & ( P_{2}[x,y] implies f . [x,y] = F_{5}(x,y) ) )

hence ( ( P_{1}[x,y] implies f . [x,y] = F_{4}(x,y) ) & ( P_{2}[x,y] implies f . [x,y] = F_{5}(x,y) ) )
by A11; :: thesis: verum

( ( P

defpred S

( not $1 = [x,y] or P

consider K being set such that

A4: for z being object holds

( z in K iff ( z in [:F

A5: for x1 being object st x1 in K holds

ex z being object st S

proof

consider f being Function such that
let x1 be object ; :: thesis: ( x1 in K implies ex z being object st S_{1}[x1,z] )

assume A6: x1 in K ; :: thesis: ex z being object st S_{1}[x1,z]

then x1 in [:F_{1}(),F_{2}():]
by A4;

then consider n9, m9 being object such that

A7: ( n9 in F_{1}() & m9 in F_{2}() )
and

A8: x1 = [n9,m9] by ZFMISC_1:def 2;

_{1}[x1,z]
; :: thesis: verum

end;assume A6: x1 in K ; :: thesis: ex z being object st S

then x1 in [:F

then consider n9, m9 being object such that

A7: ( n9 in F

A8: x1 = [n9,m9] by ZFMISC_1:def 2;

now :: thesis: ex z being object st

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

( ( P_{1}[x,y] implies z = F_{4}(x,y) ) & ( P_{2}[x,y] implies z = F_{5}(x,y) ) )end;

hence
ex z being object st Sfor x, y being object st x1 = [x,y] holds

( ( P

per cases
( P_{1}[n9,m9] or P_{2}[n9,m9] )
by A4, A6, A8;

end;

suppose A9:
P_{1}[n9,m9]
; :: thesis: ex z being object st

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

( ( P_{1}[x,y] implies z = F_{4}(x,y) ) & ( P_{2}[x,y] implies z = F_{5}(x,y) ) )

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

( ( P

take z = F_{4}(n9,m9); :: thesis: for x, y being object st x1 = [x,y] holds

( ( P_{1}[x,y] implies z = F_{4}(x,y) ) & ( P_{2}[x,y] implies z = F_{5}(x,y) ) )

let x, y be object ; :: thesis: ( x1 = [x,y] implies ( ( P_{1}[x,y] implies z = F_{4}(x,y) ) & ( P_{2}[x,y] implies z = F_{5}(x,y) ) ) )

assume x1 = [x,y] ; :: thesis: ( ( P_{1}[x,y] implies z = F_{4}(x,y) ) & ( P_{2}[x,y] implies z = F_{5}(x,y) ) )

then ( n9 = x & m9 = y ) by A8, XTUPLE_0:1;

hence ( ( P_{1}[x,y] implies z = F_{4}(x,y) ) & ( P_{2}[x,y] implies z = F_{5}(x,y) ) )
by A1, A7, A9; :: thesis: verum

end;( ( P

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

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

then ( n9 = x & m9 = y ) by A8, XTUPLE_0:1;

hence ( ( P

suppose A10:
P_{2}[n9,m9]
; :: thesis: ex z being object st

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

( ( P_{1}[x,y] implies z = F_{4}(x,y) ) & ( P_{2}[x,y] implies z = F_{5}(x,y) ) )

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

( ( P

take z = F_{5}(n9,m9); :: thesis: for x, y being object st x1 = [x,y] holds

( ( P_{1}[x,y] implies z = F_{4}(x,y) ) & ( P_{2}[x,y] implies z = F_{5}(x,y) ) )

let x, y be object ; :: thesis: ( x1 = [x,y] implies ( ( P_{1}[x,y] implies z = F_{4}(x,y) ) & ( P_{2}[x,y] implies z = F_{5}(x,y) ) ) )

assume x1 = [x,y] ; :: thesis: ( ( P_{1}[x,y] implies z = F_{4}(x,y) ) & ( P_{2}[x,y] implies z = F_{5}(x,y) ) )

then ( n9 = x & m9 = y ) by A8, XTUPLE_0:1;

hence ( ( P_{1}[x,y] implies z = F_{4}(x,y) ) & ( P_{2}[x,y] implies z = F_{5}(x,y) ) )
by A1, A7, A10; :: thesis: verum

end;( ( P

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

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

then ( n9 = x & m9 = y ) by A8, XTUPLE_0:1;

hence ( ( P

A11: ( dom f = K & ( for z being object st z in K holds

S

A12: rng f c= F

proof

K c= [:F
let z be object ; :: according to TARSKI:def 3 :: thesis: ( not z in rng f or z in F_{3}() )

assume z in rng f ; :: thesis: z in F_{3}()

then consider x1 being object such that

A13: x1 in dom f and

A14: z = f . x1 by FUNCT_1:def 3;

x1 in [:F_{1}(),F_{2}():]
by A4, A11, A13;

then consider x, y being object such that

A15: ( x in F_{1}() & y in F_{2}() )
and

A16: x1 = [x,y] by ZFMISC_1:def 2;

_{3}()
; :: thesis: verum

end;assume z in rng f ; :: thesis: z in F

then consider x1 being object such that

A13: x1 in dom f and

A14: z = f . x1 by FUNCT_1:def 3;

x1 in [:F

then consider x, y being object such that

A15: ( x in F

A16: x1 = [x,y] by ZFMISC_1:def 2;

now :: thesis: z in F_{3}()

hence
z in Fend;

then reconsider f = f as PartFunc of [:F

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

let x, y be object ; :: thesis: ( [x,y] in dom f implies ( ( P
let x, y be object ; :: thesis: ( [x,y] in dom f iff ( x in F_{1}() & y in F_{2}() & ( P_{1}[x,y] or P_{2}[x,y] ) ) )

thus ( [x,y] in dom f implies ( x in F_{1}() & y in F_{2}() & ( P_{1}[x,y] or P_{2}[x,y] ) ) )
by A4, A11, ZFMISC_1:87; :: thesis: ( x in F_{1}() & y in F_{2}() & ( P_{1}[x,y] or P_{2}[x,y] ) implies [x,y] in dom f )

assume that

A19: ( x in F_{1}() & y in F_{2}() )
and

A20: ( P_{1}[x,y] or P_{2}[x,y] )
; :: thesis: [x,y] in dom f

_{1}(),F_{2}():]
by A19, ZFMISC_1:87;

hence [x,y] in dom f by A4, A11, A21; :: thesis: verum

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

assume that

A19: ( x in F

A20: ( P

A21: now :: thesis: for z9, q9 being object holds

( not [x,y] = [z9,q9] or P_{1}[z9,q9] or P_{2}[z9,q9] )

[x,y] in [:F( not [x,y] = [z9,q9] or P

let z9, q9 be object ; :: thesis: ( not [x,y] = [z9,q9] or P_{1}[z9,q9] or P_{2}[z9,q9] )

assume A22: [x,y] = [z9,q9] ; :: thesis: ( P_{1}[z9,q9] or P_{2}[z9,q9] )

then x = z9 by XTUPLE_0:1;

hence ( P_{1}[z9,q9] or P_{2}[z9,q9] )
by A20, A22, XTUPLE_0:1; :: thesis: verum

end;assume A22: [x,y] = [z9,q9] ; :: thesis: ( P

then x = z9 by XTUPLE_0:1;

hence ( P

hence [x,y] in dom f by A4, A11, A21; :: thesis: verum

assume [x,y] in dom f ; :: thesis: ( ( P

hence ( ( P