defpred S1[ object , object ] means for x, y being object st \$1 = [x,y] holds
( ( P1[x,y] implies \$2 = F4(x,y) ) & ( P2[x,y] implies \$2 = F5(x,y) ) & ( P3[x,y] implies \$2 = F6(x,y) ) );
defpred S2[ object ] means for x, y being object holds
( not \$1 = [x,y] or P1[x,y] or P2[x,y] or P3[x,y] );
consider L being set such that
A5: for z being object holds
( z in L iff ( z in [:F1(),F2():] & S2[z] ) ) from A6: for x1 being object st x1 in L holds
ex z being object st S1[x1,z]
proof
let x1 be object ; :: thesis: ( x1 in L implies ex z being object st S1[x1,z] )
assume A7: x1 in L ; :: thesis: ex z being object st S1[x1,z]
then x1 in [:F1(),F2():] by A5;
then consider z9, a9 being object such that
A8: ( z9 in F1() & a9 in F2() ) and
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
( ( P1[x,y] implies z = F4(x,y) ) & ( P2[x,y] implies z = F5(x,y) ) & ( P3[x,y] implies z = F6(x,y) ) )
per cases ( P1[z9,a9] or P2[z9,a9] or P3[z9,a9] ) by A5, A7, A9;
suppose A10: P1[z9,a9] ; :: thesis: ex z being object st
for x, y being object st x1 = [x,y] holds
( ( P1[x,y] implies z = F4(x,y) ) & ( P2[x,y] implies z = F5(x,y) ) & ( P3[x,y] implies z = F6(x,y) ) )

take z = F4(z9,a9); :: thesis: for x, y being object st x1 = [x,y] holds
( ( P1[x,y] implies z = F4(x,y) ) & ( P2[x,y] implies z = F5(x,y) ) & ( P3[x,y] implies z = F6(x,y) ) )

let x, y be object ; :: thesis: ( x1 = [x,y] implies ( ( P1[x,y] implies z = F4(x,y) ) & ( P2[x,y] implies z = F5(x,y) ) & ( P3[x,y] implies z = F6(x,y) ) ) )
assume x1 = [x,y] ; :: thesis: ( ( P1[x,y] implies z = F4(x,y) ) & ( P2[x,y] implies z = F5(x,y) ) & ( P3[x,y] implies z = F6(x,y) ) )
then ( z9 = x & a9 = y ) by ;
hence ( ( P1[x,y] implies z = F4(x,y) ) & ( P2[x,y] implies z = F5(x,y) ) & ( P3[x,y] implies z = F6(x,y) ) ) by A1, A8, A10; :: thesis: verum
end;
suppose A11: P2[z9,a9] ; :: thesis: ex z being object st
for x, y being object st x1 = [x,y] holds
( ( P1[x,y] implies z = F4(x,y) ) & ( P2[x,y] implies z = F5(x,y) ) & ( P3[x,y] implies z = F6(x,y) ) )

take z = F5(z9,a9); :: thesis: for x, y being object st x1 = [x,y] holds
( ( P1[x,y] implies z = F4(x,y) ) & ( P2[x,y] implies z = F5(x,y) ) & ( P3[x,y] implies z = F6(x,y) ) )

let x, y be object ; :: thesis: ( x1 = [x,y] implies ( ( P1[x,y] implies z = F4(x,y) ) & ( P2[x,y] implies z = F5(x,y) ) & ( P3[x,y] implies z = F6(x,y) ) ) )
assume x1 = [x,y] ; :: thesis: ( ( P1[x,y] implies z = F4(x,y) ) & ( P2[x,y] implies z = F5(x,y) ) & ( P3[x,y] implies z = F6(x,y) ) )
then ( z9 = x & a9 = y ) by ;
hence ( ( P1[x,y] implies z = F4(x,y) ) & ( P2[x,y] implies z = F5(x,y) ) & ( P3[x,y] implies z = F6(x,y) ) ) by A1, A8, A11; :: thesis: verum
end;
suppose A12: P3[z9,a9] ; :: thesis: ex z being object st
for x, y being object st x1 = [x,y] holds
( ( P1[x,y] implies z = F4(x,y) ) & ( P2[x,y] implies z = F5(x,y) ) & ( P3[x,y] implies z = F6(x,y) ) )

take z = F6(z9,a9); :: thesis: for x, y being object st x1 = [x,y] holds
( ( P1[x,y] implies z = F4(x,y) ) & ( P2[x,y] implies z = F5(x,y) ) & ( P3[x,y] implies z = F6(x,y) ) )

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

thus for x, y being object holds
( [x,y] in dom f iff ( x in F1() & y in F2() & ( P1[x,y] or P2[x,y] or P3[x,y] ) ) ) :: thesis: for x, y being object st [x,y] in dom f holds
( ( P1[x,y] implies f . [x,y] = F4(x,y) ) & ( P2[x,y] implies f . [x,y] = F5(x,y) ) & ( P3[x,y] implies f . [x,y] = F6(x,y) ) )
proof
let x, y be object ; :: thesis: ( [x,y] in dom f iff ( x in F1() & y in F2() & ( P1[x,y] or P2[x,y] or P3[x,y] ) ) )
thus ( [x,y] in dom f implies ( x in F1() & y in F2() & ( P1[x,y] or P2[x,y] or P3[x,y] ) ) ) by ; :: thesis: ( x in F1() & y in F2() & ( P1[x,y] or P2[x,y] or P3[x,y] ) implies [x,y] in dom f )
assume that
A22: ( x in F1() & y in F2() ) and
A23: ( P1[x,y] or P2[x,y] or P3[x,y] ) ; :: thesis: [x,y] in dom f
A24: now :: thesis: for f9, r9 being object holds
( not [x,y] = [f9,r9] or P1[f9,r9] or P2[f9,r9] or P3[f9,r9] )
let f9, r9 be object ; :: thesis: ( not [x,y] = [f9,r9] or P1[f9,r9] or P2[f9,r9] or P3[f9,r9] )
assume A25: [x,y] = [f9,r9] ; :: thesis: ( P1[f9,r9] or P2[f9,r9] or P3[f9,r9] )
then x = f9 by XTUPLE_0:1;
hence ( P1[f9,r9] or P2[f9,r9] or P3[f9,r9] ) by A23, A25, XTUPLE_0:1; :: thesis: verum
end;
[x,y] in [:F1(),F2():] by ;
hence [x,y] in dom f by A5, A13, A24; :: thesis: verum
end;
let x, y be object ; :: thesis: ( [x,y] in dom f implies ( ( P1[x,y] implies f . [x,y] = F4(x,y) ) & ( P2[x,y] implies f . [x,y] = F5(x,y) ) & ( P3[x,y] implies f . [x,y] = F6(x,y) ) ) )
assume [x,y] in dom f ; :: thesis: ( ( P1[x,y] implies f . [x,y] = F4(x,y) ) & ( P2[x,y] implies f . [x,y] = F5(x,y) ) & ( P3[x,y] implies f . [x,y] = F6(x,y) ) )
hence ( ( P1[x,y] implies f . [x,y] = F4(x,y) ) & ( P2[x,y] implies f . [x,y] = F5(x,y) ) & ( P3[x,y] implies f . [x,y] = F6(x,y) ) ) by A13; :: thesis: verum