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) ) );
defpred S2[ object ] means for x, y being object holds
( not $1 = [x,y] or P1[x,y] or P2[x,y] );
consider K being set such that
A4: for z being object holds
( z in K iff ( z in [:F1(),F2():] & S2[z] ) ) from XBOOLE_0:sch 1();
 A5: for x1 being object st x1 in K holds
ex z being object st S1[x1,z]
proof
let x1 be object ; :: thesis: ( x1 in K implies ex z being object st S1[x1,z] )
assume A6: x1 in K ; :: thesis: ex z being object st S1[x1,z]
then x1 in [:F1(),F2():] by A4;
then consider n9, m9 being object such that
A7: ( n9 in F1() & m9 in F2() ) and
A8: x1 = [n9,m9] 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) ) )
per cases ( P1[n9,m9] or P2[n9,m9] ) by A4, A6, A8;
suppose A9: P1[n9,m9] ; :: 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) ) )
take z = F4(n9,m9); :: 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) ) )
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) ) ) )
assume x1 = [x,y] ; :: thesis: ( ( P1[x,y] implies z = F4(x,y) ) & ( P2[x,y] implies z = F5(x,y) ) )
then ( n9 = x & m9 = y ) by A8, XTUPLE_0:1;
hence ( ( P1[x,y] implies z = F4(x,y) ) & ( P2[x,y] implies z = F5(x,y) ) ) by A1, A7, A9; :: thesis: verum
end;
suppose A10: P2[n9,m9] ; :: 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) ) )
take z = F5(n9,m9); :: 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) ) )
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) ) ) )
assume x1 = [x,y] ; :: thesis: ( ( P1[x,y] implies z = F4(x,y) ) & ( P2[x,y] implies z = F5(x,y) ) )
then ( n9 = x & m9 = y ) by A8, XTUPLE_0:1;
hence ( ( P1[x,y] implies z = F4(x,y) ) & ( P2[x,y] implies z = F5(x,y) ) ) by A1, A7, A10; :: 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 = K & ( for z being object st z in K holds
S1[z,f . z] ) ) from CLASSES1:sch 1(A5);
 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 A4, A11, A13;
then consider x, y being object such that
A15: ( x in F1() & y in F2() ) and
A16: x1 = [x,y] by ZFMISC_1:def 2;
now :: thesis: z in F3()
end;
hence z in F3() ; :: thesis: verum
end;
K c= [:F1(),F2():] by A4;
then reconsider f = f as PartFunc of [:F1(),F2():],F3() by A11, A12, RELSET_1:4;
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] ) ) ) ) & ( 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) ) ) ) )
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] ) ) ) :: 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) ) )
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] ) ) )
thus ( [x,y] in dom f implies ( x in F1() & y in F2() & ( P1[x,y] or P2[x,y] ) ) ) by A4, A11, ZFMISC_1:87; :: thesis: ( x in F1() & y in F2() & ( P1[x,y] or P2[x,y] ) implies [x,y] in dom f )
assume that
A19: ( x in F1() & y in F2() ) and
A20: ( P1[x,y] or P2[x,y] ) ; :: thesis: [x,y] in dom f
A21: now :: thesis: for z9, q9 being object holds
( not [x,y] = [z9,q9] or P1[z9,q9] or P2[z9,q9] )
let z9, q9 be object ; :: thesis: ( not [x,y] = [z9,q9] or P1[z9,q9] or P2[z9,q9] )
assume A22: [x,y] = [z9,q9] ; :: thesis: ( P1[z9,q9] or P2[z9,q9] )
then x = z9 by XTUPLE_0:1;
hence ( P1[z9,q9] or P2[z9,q9] ) by A20, A22, XTUPLE_0:1; :: thesis: verum
end;
[x,y] in [:F1(),F2():] by A19, ZFMISC_1:87;
hence [x,y] in dom f by A4, A11, A21; :: 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) ) ) )
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) ) )
hence ( ( P1[x,y] implies f . [x,y] = F4(x,y) ) & ( P2[x,y] implies f . [x,y] = F5(x,y) ) ) by A11; :: thesis: verum