defpred S1[ object , object ] means for c being Element of F1()
for t being Element of F2() st $1 = [c,t] holds
( ( P1[c,t] implies $2 = F4(c,t) ) & ( P2[c,t] implies $2 = F5(c,t) ) );
defpred S2[ object ] means for c being Element of F1()
for d being Element of F2() holds
( not $1 = [c,d] or P1[c,d] or P2[c,d] );
consider F being set such that
A2: for z being object holds
( z in F iff ( z in [:F1(),F2():] & S2[z] ) ) from XBOOLE_0:sch 1();
 A3: for x1 being object st x1 in F holds
ex z being object st S1[x1,z]
proof
let x1 be object ; :: thesis: ( x1 in F implies ex z being object st S1[x1,z] )
assume A4: x1 in F ; :: thesis: ex z being object st S1[x1,z]
then x1 in [:F1(),F2():] by A2;
then consider f9, g9 being object such that
A5: f9 in F1() and
A6: g9 in F2() and
A7: x1 = [f9,g9] by ZFMISC_1:def 2;
reconsider g9 = g9 as Element of F2() by A6;
reconsider f9 = f9 as Element of F1() by A5;
now :: thesis: ex z being Element of F3() st
for p being Element of F1()
for d being Element of F2() st x1 = [p,d] holds
( ( P1[p,d] implies z = F4(p,d) ) & ( P2[p,d] implies z = F5(p,d) ) )
per cases ( P1[f9,g9] or P2[f9,g9] ) by A2, A4, A7;
suppose A8: P1[f9,g9] ; :: thesis: ex z being Element of F3() st
for p being Element of F1()
for d being Element of F2() st x1 = [p,d] holds
( ( P1[p,d] implies z = F4(p,d) ) & ( P2[p,d] implies z = F5(p,d) ) )
take z = F4(f9,g9); :: thesis: for p being Element of F1()
for d being Element of F2() st x1 = [p,d] holds
( ( P1[p,d] implies z = F4(p,d) ) & ( P2[p,d] implies z = F5(p,d) ) )
let p be Element of F1(); :: thesis: for d being Element of F2() st x1 = [p,d] holds
( ( P1[p,d] implies z = F4(p,d) ) & ( P2[p,d] implies z = F5(p,d) ) )
let d be Element of F2(); :: thesis: ( x1 = [p,d] implies ( ( P1[p,d] implies z = F4(p,d) ) & ( P2[p,d] implies z = F5(p,d) ) ) )
assume x1 = [p,d] ; :: thesis: ( ( P1[p,d] implies z = F4(p,d) ) & ( P2[p,d] implies z = F5(p,d) ) )
then ( f9 = p & g9 = d ) by A7, XTUPLE_0:1;
hence ( ( P1[p,d] implies z = F4(p,d) ) & ( P2[p,d] implies z = F5(p,d) ) ) by A1, A8; :: thesis: verum
end;
suppose A9: P2[f9,g9] ; :: thesis: ex z being Element of F3() st
for r being Element of F1()
for d being Element of F2() st x1 = [r,d] holds
( ( P1[r,d] implies z = F4(r,d) ) & ( P2[r,d] implies z = F5(r,d) ) )
take z = F5(f9,g9); :: thesis: for r being Element of F1()
for d being Element of F2() st x1 = [r,d] holds
( ( P1[r,d] implies z = F4(r,d) ) & ( P2[r,d] implies z = F5(r,d) ) )
let r be Element of F1(); :: thesis: for d being Element of F2() st x1 = [r,d] holds
( ( P1[r,d] implies z = F4(r,d) ) & ( P2[r,d] implies z = F5(r,d) ) )
let d be Element of F2(); :: thesis: ( x1 = [r,d] implies ( ( P1[r,d] implies z = F4(r,d) ) & ( P2[r,d] implies z = F5(r,d) ) ) )
assume x1 = [r,d] ; :: thesis: ( ( P1[r,d] implies z = F4(r,d) ) & ( P2[r,d] implies z = F5(r,d) ) )
then ( f9 = r & g9 = d ) by A7, XTUPLE_0:1;
hence ( ( P1[r,d] implies z = F4(r,d) ) & ( P2[r,d] implies z = F5(r,d) ) ) by A1, A9; :: thesis: verum
end;
end;
end;
hence ex z being object st S1[x1,z] ; :: thesis: verum
end;
consider f being Function such that
A10: ( dom f = F & ( for z being object st z in F holds
S1[z,f . z] ) ) from CLASSES1:sch 1(A3);
 A11: rng f c= F3()
proof
let z be object ; :: according to TARSKI:def 3 :: thesis: ( not z in rng f or z in F3() )
assume z in rng f ; :: thesis: z in F3()
then consider x1 being object such that
A12: x1 in dom f and
A13: z = f . x1 by FUNCT_1:def 3;
x1 in [:F1(),F2():] by A2, A10, A12;
then consider x, y being object such that
A14: x in F1() and
A15: y in F2() and
A16: x1 = [x,y] by ZFMISC_1:def 2;
reconsider y = y as Element of F2() by A15;
reconsider x = x as Element of F1() by A14;
now :: thesis: z in F3()
end;
hence z in F3() ; :: thesis: verum
end;
F c= [:F1(),F2():] by A2;
then reconsider f = f as PartFunc of [:F1(),F2():],F3() by A10, A11, RELSET_1:4;
take f ; :: thesis: ( ( for c being Element of F1()
for d being Element of F2() holds
( [c,d] in dom f iff ( P1[c,d] or P2[c,d] ) ) ) & ( for c being Element of F1()
for d being Element of F2() st [c,d] in dom f holds
( ( P1[c,d] implies f . [c,d] = F4(c,d) ) & ( P2[c,d] implies f . [c,d] = F5(c,d) ) ) ) )
thus for c being Element of F1()
for h being Element of F2() holds
( [c,h] in dom f iff ( P1[c,h] or P2[c,h] ) ) :: thesis: for c being Element of F1()
for d being Element of F2() st [c,d] in dom f holds
( ( P1[c,d] implies f . [c,d] = F4(c,d) ) & ( P2[c,d] implies f . [c,d] = F5(c,d) ) )
proof
let c be Element of F1(); :: thesis: for h being Element of F2() holds
( [c,h] in dom f iff ( P1[c,h] or P2[c,h] ) )
let g be Element of F2(); :: thesis: ( [c,g] in dom f iff ( P1[c,g] or P2[c,g] ) )
thus ( not [c,g] in dom f or P1[c,g] or P2[c,g] ) by A2, A10; :: thesis: ( ( P1[c,g] or P2[c,g] ) implies [c,g] in dom f )
assume A17: ( P1[c,g] or P2[c,g] ) ; :: thesis: [c,g] in dom f
A18: now :: thesis: for h9 being Element of F1()
for j9 being Element of F2() holds
( not [c,g] = [h9,j9] or P1[h9,j9] or P2[h9,j9] )
let h9 be Element of F1(); :: thesis: for j9 being Element of F2() holds
( not [c,g] = [h9,j9] or P1[h9,j9] or P2[h9,j9] )
let j9 be Element of F2(); :: thesis: ( not [c,g] = [h9,j9] or P1[h9,j9] or P2[h9,j9] )
assume A19: [c,g] = [h9,j9] ; :: thesis: ( P1[h9,j9] or P2[h9,j9] )
then c = h9 by XTUPLE_0:1;
hence ( P1[h9,j9] or P2[h9,j9] ) by A17, A19, XTUPLE_0:1; :: thesis: verum
end;
[c,g] in [:F1(),F2():] by ZFMISC_1:87;
hence [c,g] in dom f by A2, A10, A18; :: thesis: verum
end;
let c be Element of F1(); :: thesis: for d being Element of F2() st [c,d] in dom f holds
( ( P1[c,d] implies f . [c,d] = F4(c,d) ) & ( P2[c,d] implies f . [c,d] = F5(c,d) ) )
let d be Element of F2(); :: thesis: ( [c,d] in dom f implies ( ( P1[c,d] implies f . [c,d] = F4(c,d) ) & ( P2[c,d] implies f . [c,d] = F5(c,d) ) ) )
assume [c,d] in dom f ; :: thesis: ( ( P1[c,d] implies f . [c,d] = F4(c,d) ) & ( P2[c,d] implies f . [c,d] = F5(c,d) ) )
hence ( ( P1[c,d] implies f . [c,d] = F4(c,d) ) & ( P2[c,d] implies f . [c,d] = F5(c,d) ) ) by A10; :: thesis: verum