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) ) );

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] );

consider F being set such that

A2: for z being object holds

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

A3: for x1 being object st x1 in F holds

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

A10: ( dom f = F & ( for z being object st z in F holds

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

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

then reconsider f = f as PartFunc of [:F_{1}(),F_{2}():],F_{3}() by A10, A11, 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] ) ) ) & ( for c being Element of F_{1}()

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

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

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

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

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

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

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

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

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) ) ) )

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) ) )

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) ) )
by A10; :: thesis: verum

for t being Element of F

( ( P

defpred S

for d being Element of F

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

consider F being set such that

A2: for z being object holds

( z in F iff ( z in [:F

A3: for x1 being object st x1 in F holds

ex z being object st S

proof

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

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

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

then consider f9, g9 being object such that

A5: f9 in F_{1}()
and

A6: g9 in F_{2}()
and

A7: x1 = [f9,g9] by ZFMISC_1:def 2;

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

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

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

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

then x1 in [:F

then consider f9, g9 being object such that

A5: f9 in F

A6: g9 in F

A7: x1 = [f9,g9] by ZFMISC_1:def 2;

reconsider g9 = g9 as Element of F

reconsider f9 = f9 as Element of F

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

for p being Element of F_{1}()

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

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

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

for d being Element of F

( ( P

per cases
( P_{1}[f9,g9] or P_{2}[f9,g9] )
by A2, A4, A7;

end;

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

for p being Element of F_{1}()

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

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

for p being Element of F

for d being Element of F

( ( P

take z = F_{4}(f9,g9); :: thesis: for p being Element of F_{1}()

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

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

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

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

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

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

then ( f9 = p & g9 = d ) by A7, XTUPLE_0:1;

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

end;for d being Element of F

( ( P

let p be Element of F

( ( P

let d be Element of F

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

then ( f9 = p & g9 = d ) by A7, XTUPLE_0:1;

hence ( ( P

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

for r being Element of F_{1}()

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

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

for r being Element of F

for d being Element of F

( ( P

take z = F_{5}(f9,g9); :: thesis: for r being Element of F_{1}()

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

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

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

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

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

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

then ( f9 = r & g9 = d ) by A7, XTUPLE_0:1;

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

end;for d being Element of F

( ( P

let r be Element of F

( ( P

let d be Element of F

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

then ( f9 = r & g9 = d ) by A7, XTUPLE_0:1;

hence ( ( P

A10: ( dom f = F & ( for z being object st z in F holds

S

A11: rng f c= F

proof

F 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

A12: x1 in dom f and

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

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

then consider x, y being object such that

A14: x in F_{1}()
and

A15: y in F_{2}()
and

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

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

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

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

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

then consider x1 being object such that

A12: x1 in dom f and

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

x1 in [:F

then consider x, y being object such that

A14: x in F

A15: y in F

A16: 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] )
by A2, A10, A12, A16;

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 d being Element of F

( ( P

thus for c being Element of F

for h being Element of F

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

for d being Element of F

( ( P

proof

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

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

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

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

assume A17: ( P_{1}[c,g] or P_{2}[c,g] )
; :: thesis: [c,g] in dom f

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

hence [c,g] in dom f by A2, A10, A18; :: thesis: verum

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

let g be Element of F

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

assume A17: ( P

A18: now :: thesis: for h9 being Element of F_{1}()

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

( not [c,g] = [h9,j9] or P_{1}[h9,j9] or P_{2}[h9,j9] )

[c,g] in [:Ffor j9 being Element of F

( not [c,g] = [h9,j9] or P

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

( not [c,g] = [h9,j9] or P_{1}[h9,j9] or P_{2}[h9,j9] )

let j9 be Element of F_{2}(); :: thesis: ( not [c,g] = [h9,j9] or P_{1}[h9,j9] or P_{2}[h9,j9] )

assume A19: [c,g] = [h9,j9] ; :: thesis: ( P_{1}[h9,j9] or P_{2}[h9,j9] )

then c = h9 by XTUPLE_0:1;

hence ( P_{1}[h9,j9] or P_{2}[h9,j9] )
by A17, A19, XTUPLE_0:1; :: thesis: verum

end;( not [c,g] = [h9,j9] or P

let j9 be Element of F

assume A19: [c,g] = [h9,j9] ; :: thesis: ( P

then c = h9 by XTUPLE_0:1;

hence ( P

hence [c,g] in dom f by A2, A10, A18; :: thesis: verum

( ( P

let d be Element of F

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

hence ( ( P