defpred S_{1}[ object , object ] means for c being Element of F_{1}()

for t being Element of F_{2}() st $1 = [c,t] holds

( ( P_{1}[c,t] implies $2 = F_{4}(c,t) ) & ( P_{2}[c,t] implies $2 = F_{5}(c,t) ) & ( P_{3}[c,t] implies $2 = F_{6}(c,t) ) );

defpred S_{2}[ object ] means for c being Element of F_{1}()

for d being Element of F_{2}() holds

( not $1 = [c,d] or P_{1}[c,d] or P_{2}[c,d] or P_{3}[c,d] );

consider T being set such that

A2: for z being object holds

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

A3: for x1 being object st x1 in T holds

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

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

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

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

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

take f ; :: thesis: ( ( for c being Element of F_{1}()

for d being Element of F_{2}() holds

( [c,d] in dom f iff ( P_{1}[c,d] or P_{2}[c,d] or P_{3}[c,d] ) ) ) & ( for c being Element of F_{1}()

for r being Element of F_{2}() st [c,r] in dom f holds

( ( P_{1}[c,r] implies f . [c,r] = F_{4}(c,r) ) & ( P_{2}[c,r] implies f . [c,r] = F_{5}(c,r) ) & ( P_{3}[c,r] implies f . [c,r] = F_{6}(c,r) ) ) ) )

thus for c being Element of F_{1}()

for d being Element of F_{2}() holds

( [c,d] in dom f iff ( P_{1}[c,d] or P_{2}[c,d] or P_{3}[c,d] ) )
:: thesis: for c being Element of F_{1}()

for r being Element of F_{2}() st [c,r] in dom f holds

( ( P_{1}[c,r] implies f . [c,r] = F_{4}(c,r) ) & ( P_{2}[c,r] implies f . [c,r] = F_{5}(c,r) ) & ( P_{3}[c,r] implies f . [c,r] = F_{6}(c,r) ) )_{1}(); :: thesis: for r being Element of F_{2}() st [c,r] in dom f holds

( ( P_{1}[c,r] implies f . [c,r] = F_{4}(c,r) ) & ( P_{2}[c,r] implies f . [c,r] = F_{5}(c,r) ) & ( P_{3}[c,r] implies f . [c,r] = F_{6}(c,r) ) )

let d be Element of F_{2}(); :: thesis: ( [c,d] in dom f implies ( ( P_{1}[c,d] implies f . [c,d] = F_{4}(c,d) ) & ( P_{2}[c,d] implies f . [c,d] = F_{5}(c,d) ) & ( P_{3}[c,d] implies f . [c,d] = F_{6}(c,d) ) ) )

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

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

for t being Element of F

( ( P

defpred S

for d being Element of F

( not $1 = [c,d] or P

consider T being set such that

A2: for z being object holds

( z in T iff ( z in [:F

A3: for x1 being object st x1 in T holds

ex z being object st S

proof

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

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

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

then consider q9, w9 being object such that

A5: q9 in F_{1}()
and

A6: w9 in F_{2}()
and

A7: x1 = [q9,w9] by ZFMISC_1:def 2;

reconsider w9 = w9 as Element of F_{2}() by A6;

reconsider q9 = q9 as Element of F_{1}() by A5;

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

end;assume A4: x1 in T ; :: thesis: ex z being object st S

then x1 in [:F

then consider q9, w9 being object such that

A5: q9 in F

A6: w9 in F

A7: x1 = [q9,w9] by ZFMISC_1:def 2;

reconsider w9 = w9 as Element of F

reconsider q9 = q9 as Element of F

now :: thesis: ex z being Element of F_{3}() st

for c being Element of F_{1}()

for d being Element of F_{2}() st x1 = [c,d] holds

( ( P_{1}[c,d] implies z = F_{4}(c,d) ) & ( P_{2}[c,d] implies z = F_{5}(c,d) ) & ( P_{3}[c,d] implies z = F_{6}(c,d) ) )end;

hence
ex z being object st Sfor c being Element of F

for d being Element of F

( ( P

per cases
( P_{1}[q9,w9] or P_{2}[q9,w9] or P_{3}[q9,w9] )
by A2, A4, A7;

end;

suppose A8:
P_{1}[q9,w9]
; :: thesis: ex z being Element of F_{3}() st

for c being Element of F_{1}()

for d being Element of F_{2}() st x1 = [c,d] holds

( ( P_{1}[c,d] implies z = F_{4}(c,d) ) & ( P_{2}[c,d] implies z = F_{5}(c,d) ) & ( P_{3}[c,d] implies z = F_{6}(c,d) ) )

for c being Element of F

for d being Element of F

( ( P

take z = F_{4}(q9,w9); :: thesis: for c being Element of F_{1}()

for d being Element of F_{2}() st x1 = [c,d] holds

( ( P_{1}[c,d] implies z = F_{4}(c,d) ) & ( P_{2}[c,d] implies z = F_{5}(c,d) ) & ( P_{3}[c,d] implies z = F_{6}(c,d) ) )

let c be Element of F_{1}(); :: thesis: for d being Element of F_{2}() st x1 = [c,d] holds

( ( P_{1}[c,d] implies z = F_{4}(c,d) ) & ( P_{2}[c,d] implies z = F_{5}(c,d) ) & ( P_{3}[c,d] implies z = F_{6}(c,d) ) )

let d be Element of F_{2}(); :: thesis: ( x1 = [c,d] implies ( ( P_{1}[c,d] implies z = F_{4}(c,d) ) & ( P_{2}[c,d] implies z = F_{5}(c,d) ) & ( P_{3}[c,d] implies z = F_{6}(c,d) ) ) )

assume x1 = [c,d] ; :: thesis: ( ( P_{1}[c,d] implies z = F_{4}(c,d) ) & ( P_{2}[c,d] implies z = F_{5}(c,d) ) & ( P_{3}[c,d] implies z = F_{6}(c,d) ) )

then ( q9 = c & w9 = d ) by A7, XTUPLE_0:1;

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

end;for d being Element of F

( ( P

let c be Element of F

( ( P

let d be Element of F

assume x1 = [c,d] ; :: thesis: ( ( P

then ( q9 = c & w9 = d ) by A7, XTUPLE_0:1;

hence ( ( P

suppose A9:
P_{2}[q9,w9]
; :: thesis: ex z being Element of F_{3}() st

for c being Element of F_{1}()

for d being Element of F_{2}() st x1 = [c,d] holds

( ( P_{1}[c,d] implies z = F_{4}(c,d) ) & ( P_{2}[c,d] implies z = F_{5}(c,d) ) & ( P_{3}[c,d] implies z = F_{6}(c,d) ) )

for c being Element of F

for d being Element of F

( ( P

take z = F_{5}(q9,w9); :: thesis: for c being Element of F_{1}()

for d being Element of F_{2}() st x1 = [c,d] holds

( ( P_{1}[c,d] implies z = F_{4}(c,d) ) & ( P_{2}[c,d] implies z = F_{5}(c,d) ) & ( P_{3}[c,d] implies z = F_{6}(c,d) ) )

let c be Element of F_{1}(); :: thesis: for d being Element of F_{2}() st x1 = [c,d] holds

( ( P_{1}[c,d] implies z = F_{4}(c,d) ) & ( P_{2}[c,d] implies z = F_{5}(c,d) ) & ( P_{3}[c,d] implies z = F_{6}(c,d) ) )

let d be Element of F_{2}(); :: thesis: ( x1 = [c,d] implies ( ( P_{1}[c,d] implies z = F_{4}(c,d) ) & ( P_{2}[c,d] implies z = F_{5}(c,d) ) & ( P_{3}[c,d] implies z = F_{6}(c,d) ) ) )

assume x1 = [c,d] ; :: thesis: ( ( P_{1}[c,d] implies z = F_{4}(c,d) ) & ( P_{2}[c,d] implies z = F_{5}(c,d) ) & ( P_{3}[c,d] implies z = F_{6}(c,d) ) )

then ( q9 = c & w9 = d ) by A7, XTUPLE_0:1;

hence ( ( P_{1}[c,d] implies z = F_{4}(c,d) ) & ( P_{2}[c,d] implies z = F_{5}(c,d) ) & ( P_{3}[c,d] implies z = F_{6}(c,d) ) )
by A1, A9; :: thesis: verum

end;for d being Element of F

( ( P

let c be Element of F

( ( P

let d be Element of F

assume x1 = [c,d] ; :: thesis: ( ( P

then ( q9 = c & w9 = d ) by A7, XTUPLE_0:1;

hence ( ( P

suppose A10:
P_{3}[q9,w9]
; :: thesis: ex z being Element of F_{3}() st

for c being Element of F_{1}()

for d being Element of F_{2}() st x1 = [c,d] holds

( ( P_{1}[c,d] implies z = F_{4}(c,d) ) & ( P_{2}[c,d] implies z = F_{5}(c,d) ) & ( P_{3}[c,d] implies z = F_{6}(c,d) ) )

for c being Element of F

for d being Element of F

( ( P

take z = F_{6}(q9,w9); :: thesis: for c being Element of F_{1}()

for d being Element of F_{2}() st x1 = [c,d] holds

( ( P_{1}[c,d] implies z = F_{4}(c,d) ) & ( P_{2}[c,d] implies z = F_{5}(c,d) ) & ( P_{3}[c,d] implies z = F_{6}(c,d) ) )

let c be Element of F_{1}(); :: thesis: for d being Element of F_{2}() st x1 = [c,d] holds

( ( P_{1}[c,d] implies z = F_{4}(c,d) ) & ( P_{2}[c,d] implies z = F_{5}(c,d) ) & ( P_{3}[c,d] implies z = F_{6}(c,d) ) )

let d be Element of F_{2}(); :: thesis: ( x1 = [c,d] implies ( ( P_{1}[c,d] implies z = F_{4}(c,d) ) & ( P_{2}[c,d] implies z = F_{5}(c,d) ) & ( P_{3}[c,d] implies z = F_{6}(c,d) ) ) )

assume x1 = [c,d] ; :: thesis: ( ( P_{1}[c,d] implies z = F_{4}(c,d) ) & ( P_{2}[c,d] implies z = F_{5}(c,d) ) & ( P_{3}[c,d] implies z = F_{6}(c,d) ) )

then ( q9 = c & w9 = d ) by A7, XTUPLE_0:1;

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

end;for d being Element of F

( ( P

let c be Element of F

( ( P

let d be Element of F

assume x1 = [c,d] ; :: thesis: ( ( P

then ( q9 = c & w9 = d ) by A7, XTUPLE_0:1;

hence ( ( P

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

S

A12: rng f c= F

proof

T 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 A2, A11, A13;

then consider x, y being object such that

A15: x in F_{1}()
and

A16: y in F_{2}()
and

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

reconsider y = y as Element of F_{2}() by A16;

reconsider x = x as Element of F_{1}() by A15;

_{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: y in F

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

reconsider y = y as Element of F

reconsider x = x as Element of F

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 A2, A11, A13, A17;

end;

then reconsider f = f as PartFunc of [:F

take f ; :: thesis: ( ( for c being Element of F

for d being Element of F

( [c,d] in dom f iff ( P

for r being Element of F

( ( P

thus for c being Element of F

for d being Element of F

( [c,d] in dom f iff ( P

for r being Element of F

( ( P

proof

let c be Element of F
let c be Element of F_{1}(); :: thesis: for d being Element of F_{2}() holds

( [c,d] in dom f iff ( P_{1}[c,d] or P_{2}[c,d] or P_{3}[c,d] ) )

let d be Element of F_{2}(); :: thesis: ( [c,d] in dom f iff ( P_{1}[c,d] or P_{2}[c,d] or P_{3}[c,d] ) )

thus ( not [c,d] in dom f or P_{1}[c,d] or P_{2}[c,d] or P_{3}[c,d] )
by A2, A11; :: thesis: ( ( P_{1}[c,d] or P_{2}[c,d] or P_{3}[c,d] ) implies [c,d] in dom f )

assume A18: ( P_{1}[c,d] or P_{2}[c,d] or P_{3}[c,d] )
; :: thesis: [c,d] in dom f

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

hence [c,d] in dom f by A2, A11, A19; :: thesis: verum

end;( [c,d] in dom f iff ( P

let d be Element of F

thus ( not [c,d] in dom f or P

assume A18: ( P

A19: now :: thesis: for i9 being Element of F_{1}()

for o9 being Element of F_{2}() holds

( not [c,d] = [i9,o9] or P_{1}[i9,o9] or P_{2}[i9,o9] or P_{3}[i9,o9] )

[c,d] in [:Ffor o9 being Element of F

( not [c,d] = [i9,o9] or P

let i9 be Element of F_{1}(); :: thesis: for o9 being Element of F_{2}() holds

( not [c,d] = [i9,o9] or P_{1}[i9,o9] or P_{2}[i9,o9] or P_{3}[i9,o9] )

let o9 be Element of F_{2}(); :: thesis: ( not [c,d] = [i9,o9] or P_{1}[i9,o9] or P_{2}[i9,o9] or P_{3}[i9,o9] )

assume A20: [c,d] = [i9,o9] ; :: thesis: ( P_{1}[i9,o9] or P_{2}[i9,o9] or P_{3}[i9,o9] )

then c = i9 by XTUPLE_0:1;

hence ( P_{1}[i9,o9] or P_{2}[i9,o9] or P_{3}[i9,o9] )
by A18, A20, XTUPLE_0:1; :: thesis: verum

end;( not [c,d] = [i9,o9] or P

let o9 be Element of F

assume A20: [c,d] = [i9,o9] ; :: thesis: ( P

then c = i9 by XTUPLE_0:1;

hence ( P

hence [c,d] in dom f by A2, A11, A19; :: thesis: verum

( ( P

let d be Element of F

assume [c,d] in dom f ; :: thesis: ( ( P

hence ( ( P