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) ) & ( P3[c,t] implies \$2 = F6(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] or P3[c,d] );
consider T being set such that
A2: for z being object holds
( z in T iff ( z in [:F1(),F2():] & S2[z] ) ) from A3: for x1 being object st x1 in T holds
ex z being object st S1[x1,z]
proof
let x1 be object ; :: thesis: ( x1 in T implies ex z being object st S1[x1,z] )
assume A4: x1 in T ; :: thesis: ex z being object st S1[x1,z]
then x1 in [:F1(),F2():] by A2;
then consider q9, w9 being object such that
A5: q9 in F1() and
A6: w9 in F2() and
A7: x1 = [q9,w9] by ZFMISC_1:def 2;
reconsider w9 = w9 as Element of F2() by A6;
reconsider q9 = q9 as Element of F1() by A5;
now :: thesis: ex z being Element of F3() st
for c being Element of F1()
for d being Element of F2() st x1 = [c,d] holds
( ( P1[c,d] implies z = F4(c,d) ) & ( P2[c,d] implies z = F5(c,d) ) & ( P3[c,d] implies z = F6(c,d) ) )
per cases ( P1[q9,w9] or P2[q9,w9] or P3[q9,w9] ) by A2, A4, A7;
suppose A8: P1[q9,w9] ; :: thesis: ex z being Element of F3() st
for c being Element of F1()
for d being Element of F2() st x1 = [c,d] holds
( ( P1[c,d] implies z = F4(c,d) ) & ( P2[c,d] implies z = F5(c,d) ) & ( P3[c,d] implies z = F6(c,d) ) )

take z = F4(q9,w9); :: thesis: for c being Element of F1()
for d being Element of F2() st x1 = [c,d] holds
( ( P1[c,d] implies z = F4(c,d) ) & ( P2[c,d] implies z = F5(c,d) ) & ( P3[c,d] implies z = F6(c,d) ) )

let c be Element of F1(); :: thesis: for d being Element of F2() st x1 = [c,d] holds
( ( P1[c,d] implies z = F4(c,d) ) & ( P2[c,d] implies z = F5(c,d) ) & ( P3[c,d] implies z = F6(c,d) ) )

let d be Element of F2(); :: thesis: ( x1 = [c,d] implies ( ( P1[c,d] implies z = F4(c,d) ) & ( P2[c,d] implies z = F5(c,d) ) & ( P3[c,d] implies z = F6(c,d) ) ) )
assume x1 = [c,d] ; :: thesis: ( ( P1[c,d] implies z = F4(c,d) ) & ( P2[c,d] implies z = F5(c,d) ) & ( P3[c,d] implies z = F6(c,d) ) )
then ( q9 = c & w9 = d ) by ;
hence ( ( P1[c,d] implies z = F4(c,d) ) & ( P2[c,d] implies z = F5(c,d) ) & ( P3[c,d] implies z = F6(c,d) ) ) by A1, A8; :: thesis: verum
end;
suppose A9: P2[q9,w9] ; :: thesis: ex z being Element of F3() st
for c being Element of F1()
for d being Element of F2() st x1 = [c,d] holds
( ( P1[c,d] implies z = F4(c,d) ) & ( P2[c,d] implies z = F5(c,d) ) & ( P3[c,d] implies z = F6(c,d) ) )

take z = F5(q9,w9); :: thesis: for c being Element of F1()
for d being Element of F2() st x1 = [c,d] holds
( ( P1[c,d] implies z = F4(c,d) ) & ( P2[c,d] implies z = F5(c,d) ) & ( P3[c,d] implies z = F6(c,d) ) )

let c be Element of F1(); :: thesis: for d being Element of F2() st x1 = [c,d] holds
( ( P1[c,d] implies z = F4(c,d) ) & ( P2[c,d] implies z = F5(c,d) ) & ( P3[c,d] implies z = F6(c,d) ) )

let d be Element of F2(); :: thesis: ( x1 = [c,d] implies ( ( P1[c,d] implies z = F4(c,d) ) & ( P2[c,d] implies z = F5(c,d) ) & ( P3[c,d] implies z = F6(c,d) ) ) )
assume x1 = [c,d] ; :: thesis: ( ( P1[c,d] implies z = F4(c,d) ) & ( P2[c,d] implies z = F5(c,d) ) & ( P3[c,d] implies z = F6(c,d) ) )
then ( q9 = c & w9 = d ) by ;
hence ( ( P1[c,d] implies z = F4(c,d) ) & ( P2[c,d] implies z = F5(c,d) ) & ( P3[c,d] implies z = F6(c,d) ) ) by A1, A9; :: thesis: verum
end;
suppose A10: P3[q9,w9] ; :: thesis: ex z being Element of F3() st
for c being Element of F1()
for d being Element of F2() st x1 = [c,d] holds
( ( P1[c,d] implies z = F4(c,d) ) & ( P2[c,d] implies z = F5(c,d) ) & ( P3[c,d] implies z = F6(c,d) ) )

take z = F6(q9,w9); :: thesis: for c being Element of F1()
for d being Element of F2() st x1 = [c,d] holds
( ( P1[c,d] implies z = F4(c,d) ) & ( P2[c,d] implies z = F5(c,d) ) & ( P3[c,d] implies z = F6(c,d) ) )

let c be Element of F1(); :: thesis: for d being Element of F2() st x1 = [c,d] holds
( ( P1[c,d] implies z = F4(c,d) ) & ( P2[c,d] implies z = F5(c,d) ) & ( P3[c,d] implies z = F6(c,d) ) )

let d be Element of F2(); :: thesis: ( x1 = [c,d] implies ( ( P1[c,d] implies z = F4(c,d) ) & ( P2[c,d] implies z = F5(c,d) ) & ( P3[c,d] implies z = F6(c,d) ) ) )
assume x1 = [c,d] ; :: thesis: ( ( P1[c,d] implies z = F4(c,d) ) & ( P2[c,d] implies z = F5(c,d) ) & ( P3[c,d] implies z = F6(c,d) ) )
then ( q9 = c & w9 = d ) by ;
hence ( ( P1[c,d] implies z = F4(c,d) ) & ( P2[c,d] implies z = F5(c,d) ) & ( P3[c,d] implies z = F6(c,d) ) ) by ; :: thesis: verum
end;
end;
end;
hence ex z being object st S1[x1,z] ; :: thesis: verum
end;
consider f being Function such that
A11: ( dom f = T & ( for z being object st z in T holds
S1[z,f . z] ) ) from A12: 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
A13: x1 in dom f and
A14: z = f . x1 by FUNCT_1:def 3;
x1 in [:F1(),F2():] by A2, A11, A13;
then consider x, y being object such that
A15: x in F1() and
A16: y in F2() and
A17: x1 = [x,y] by ZFMISC_1:def 2;
reconsider y = y as Element of F2() by A16;
reconsider x = x as Element of F1() by A15;
now :: thesis: z in F3()end;
hence z in F3() ; :: thesis: verum
end;
T c= [:F1(),F2():] by A2;
then reconsider f = f as PartFunc of [:F1(),F2():],F3() by ;
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] or P3[c,d] ) ) ) & ( for c being Element of F1()
for r being Element of F2() st [c,r] in dom f holds
( ( P1[c,r] implies f . [c,r] = F4(c,r) ) & ( P2[c,r] implies f . [c,r] = F5(c,r) ) & ( P3[c,r] implies f . [c,r] = F6(c,r) ) ) ) )

thus 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] or P3[c,d] ) ) :: thesis: for c being Element of F1()
for r being Element of F2() st [c,r] in dom f holds
( ( P1[c,r] implies f . [c,r] = F4(c,r) ) & ( P2[c,r] implies f . [c,r] = F5(c,r) ) & ( P3[c,r] implies f . [c,r] = F6(c,r) ) )
proof
let c be Element of F1(); :: thesis: for d being Element of F2() holds
( [c,d] in dom f iff ( P1[c,d] or P2[c,d] or P3[c,d] ) )

let d be Element of F2(); :: thesis: ( [c,d] in dom f iff ( P1[c,d] or P2[c,d] or P3[c,d] ) )
thus ( not [c,d] in dom f or P1[c,d] or P2[c,d] or P3[c,d] ) by ; :: thesis: ( ( P1[c,d] or P2[c,d] or P3[c,d] ) implies [c,d] in dom f )
assume A18: ( P1[c,d] or P2[c,d] or P3[c,d] ) ; :: thesis: [c,d] in dom f
A19: now :: thesis: for i9 being Element of F1()
for o9 being Element of F2() holds
( not [c,d] = [i9,o9] or P1[i9,o9] or P2[i9,o9] or P3[i9,o9] )
let i9 be Element of F1(); :: thesis: for o9 being Element of F2() holds
( not [c,d] = [i9,o9] or P1[i9,o9] or P2[i9,o9] or P3[i9,o9] )

let o9 be Element of F2(); :: thesis: ( not [c,d] = [i9,o9] or P1[i9,o9] or P2[i9,o9] or P3[i9,o9] )
assume A20: [c,d] = [i9,o9] ; :: thesis: ( P1[i9,o9] or P2[i9,o9] or P3[i9,o9] )
then c = i9 by XTUPLE_0:1;
hence ( P1[i9,o9] or P2[i9,o9] or P3[i9,o9] ) by A18, A20, XTUPLE_0:1; :: thesis: verum
end;
[c,d] in [:F1(),F2():] by ZFMISC_1:87;
hence [c,d] in dom f by A2, A11, A19; :: thesis: verum
end;
let c be Element of F1(); :: thesis: for r being Element of F2() st [c,r] in dom f holds
( ( P1[c,r] implies f . [c,r] = F4(c,r) ) & ( P2[c,r] implies f . [c,r] = F5(c,r) ) & ( P3[c,r] implies f . [c,r] = F6(c,r) ) )

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) ) & ( P3[c,d] implies f . [c,d] = F6(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) ) & ( P3[c,d] implies f . [c,d] = F6(c,d) ) )
hence ( ( P1[c,d] implies f . [c,d] = F4(c,d) ) & ( P2[c,d] implies f . [c,d] = F5(c,d) ) & ( P3[c,d] implies f . [c,d] = F6(c,d) ) ) by A11; :: thesis: verum