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) ) & ( P_{3}[x,y] implies $2 = F_{6}(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] or P_{3}[x,y] );

consider L being set such that

A5: for z being object holds

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

A6: for x1 being object st x1 in L holds

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

A13: ( dom f = L & ( for z being object st z in L holds

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

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

then reconsider f = f as PartFunc of [:F_{1}(),F_{2}():],F_{3}() by A13, A14, 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] or P_{3}[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) ) & ( P_{3}[x,y] implies f . [x,y] = F_{6}(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] or P_{3}[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) ) & ( P_{3}[x,y] implies f . [x,y] = F_{6}(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) ) & ( P_{3}[x,y] implies f . [x,y] = F_{6}(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) ) & ( P_{3}[x,y] implies f . [x,y] = F_{6}(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) ) & ( P_{3}[x,y] implies f . [x,y] = F_{6}(x,y) ) )
by A13; :: thesis: verum

( ( P

defpred S

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

consider L being set such that

A5: for z being object holds

( z in L iff ( z in [:F

A6: for x1 being object st x1 in L holds

ex z being object st S

proof

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

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

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

then consider z9, a9 being object such that

A8: ( z9 in F_{1}() & a9 in F_{2}() )
and

A9: x1 = [z9,a9] by ZFMISC_1:def 2;

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

end;assume A7: x1 in L ; :: thesis: ex z being object st S

then x1 in [:F

then consider z9, a9 being object such that

A8: ( z9 in F

A9: x1 = [z9,a9] 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) ) & ( P_{3}[x,y] implies z = F_{6}(x,y) ) )end;

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

( ( P

per cases
( P_{1}[z9,a9] or P_{2}[z9,a9] or P_{3}[z9,a9] )
by A5, A7, A9;

end;

suppose A10:
P_{1}[z9,a9]
; :: 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) ) & ( P_{3}[x,y] implies z = F_{6}(x,y) ) )

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

( ( P

take z = F_{4}(z9,a9); :: 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) ) & ( P_{3}[x,y] implies z = F_{6}(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) ) & ( P_{3}[x,y] implies z = F_{6}(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) ) & ( P_{3}[x,y] implies z = F_{6}(x,y) ) )

then ( z9 = x & a9 = y ) by A9, XTUPLE_0:1;

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

end;( ( P

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

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

then ( z9 = x & a9 = y ) by A9, XTUPLE_0:1;

hence ( ( P

suppose A11:
P_{2}[z9,a9]
; :: 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) ) & ( P_{3}[x,y] implies z = F_{6}(x,y) ) )

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

( ( P

take z = F_{5}(z9,a9); :: 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) ) & ( P_{3}[x,y] implies z = F_{6}(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) ) & ( P_{3}[x,y] implies z = F_{6}(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) ) & ( P_{3}[x,y] implies z = F_{6}(x,y) ) )

then ( z9 = x & a9 = y ) by A9, XTUPLE_0:1;

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

end;( ( P

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

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

then ( z9 = x & a9 = y ) by A9, XTUPLE_0:1;

hence ( ( P

suppose A12:
P_{3}[z9,a9]
; :: 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) ) & ( P_{3}[x,y] implies z = F_{6}(x,y) ) )

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

( ( P

take z = F_{6}(z9,a9); :: 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) ) & ( P_{3}[x,y] implies z = F_{6}(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) ) & ( P_{3}[x,y] implies z = F_{6}(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) ) & ( P_{3}[x,y] implies z = F_{6}(x,y) ) )

then ( z9 = x & a9 = y ) by A9, XTUPLE_0:1;

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

end;( ( P

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

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

then ( z9 = x & a9 = y ) by A9, XTUPLE_0:1;

hence ( ( P

A13: ( dom f = L & ( for z being object st z in L holds

S

A14: rng f c= F

proof

L 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

A15: x1 in dom f and

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

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

then consider x, y being object such that

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

A18: 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

A15: x1 in dom f and

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

x1 in [:F

then consider x, y being object such that

A17: ( x in F

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

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

hence
z in Fper cases
( P_{1}[x,y] or P_{2}[x,y] or P_{3}[x,y] )
by A5, A13, A15, A18;

end;

suppose A19:
P_{1}[x,y]
; :: thesis: z in F_{3}()

then
f . [x,y] = F_{4}(x,y)
by A13, A15, A18;

hence z in F_{3}()
by A2, A16, A17, A18, A19; :: thesis: verum

end;hence z in F

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] or P_{3}[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] or P_{3}[x,y] ) ) )
by A5, A13, ZFMISC_1:87; :: thesis: ( x in F_{1}() & y in F_{2}() & ( P_{1}[x,y] or P_{2}[x,y] or P_{3}[x,y] ) implies [x,y] in dom f )

assume that

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

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

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

hence [x,y] in dom f by A5, A13, A24; :: thesis: verum

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

assume that

A22: ( x in F

A23: ( P

A24: now :: thesis: for f9, r9 being object holds

( not [x,y] = [f9,r9] or P_{1}[f9,r9] or P_{2}[f9,r9] or P_{3}[f9,r9] )

[x,y] in [:F( not [x,y] = [f9,r9] or P

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

assume A25: [x,y] = [f9,r9] ; :: thesis: ( P_{1}[f9,r9] or P_{2}[f9,r9] or P_{3}[f9,r9] )

then x = f9 by XTUPLE_0:1;

hence ( P_{1}[f9,r9] or P_{2}[f9,r9] or P_{3}[f9,r9] )
by A23, A25, XTUPLE_0:1; :: thesis: verum

end;assume A25: [x,y] = [f9,r9] ; :: thesis: ( P

then x = f9 by XTUPLE_0:1;

hence ( P

hence [x,y] in dom f by A5, A13, A24; :: thesis: verum

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

hence ( ( P