defpred S₁[ set ] means for x, y being set holds
( not $1 = [x,y] or P₁[x,y] or P₂[x,y] or P₃[x,y] );
consider L being set such that
A5: for z being set holds
( z in L iff ( z in [:F₁(),F₂():] & S₁[z] ) ) from XBOOLE_0:sch 1();
A6: L c= [:F₁(),F₂():]

proof

let z be set ; :: according to TARSKI:def 3 :: thesis:
assume z in L ; :: thesis:
hence z in [:F₁(),F₂():] by A5; :: thesis:

end;

defpred S₂[ set , set ] means for x, y being set st $1 = [x,y] holds
( ( P₁[x,y] implies $2 = F₄(x,y) ) & ( P₂[x,y] implies $2 = F₅(x,y) ) & ( P₃[x,y] implies $2 = F₆(x,y) ) );
A7: for x1 being set st x1 in L holds
ex z being set st S₂[x1,z]

proof

let x1 be set ; :: thesis:
assume A8: x1 in L ; :: thesis:
then x1 in [:F₁(),F₂():] by A5;
then consider z', a' being set such that
A9: ( z' in F₁() & a' in F₂() & x1 = [z',a'] ) by ZFMISC_1:def 2;

now

per cases by A5, A8, A9;

suppose A10: P₁[z',a'] ; :: thesis:

take z = F₄(z',a'); :: thesis:
let x, y be set ; :: thesis:
assume x1 = [x,y] ; :: thesis:
then ( z' = x & a' = y ) by A9, ZFMISC_1:33;
hence ( ( P₁[x,y] implies z = F₄(x,y) ) & ( P₂[x,y] implies z = F₅(x,y) ) & ( P₃[x,y] implies z = F₆(x,y) ) ) by A1, A9, A10; :: thesis:

end;

suppose A11: P₂[z',a'] ; :: thesis:

take z = F₅(z',a'); :: thesis:
let x, y be set ; :: thesis:
assume x1 = [x,y] ; :: thesis:
then ( z' = x & a' = y ) by A9, ZFMISC_1:33;
hence ( ( P₁[x,y] implies z = F₄(x,y) ) & ( P₂[x,y] implies z = F₅(x,y) ) & ( P₃[x,y] implies z = F₆(x,y) ) ) by A1, A9, A11; :: thesis:

end;

suppose A12: P₃[z',a'] ; :: thesis:

take z = F₆(z',a'); :: thesis:
let x, y be set ; :: thesis:
assume x1 = [x,y] ; :: thesis:
then ( z' = x & a' = y ) by A9, ZFMISC_1:33;
hence ( ( P₁[x,y] implies z = F₄(x,y) ) & ( P₂[x,y] implies z = F₅(x,y) ) & ( P₃[x,y] implies z = F₆(x,y) ) ) by A1, A9, A12; :: thesis:

end;

hence ex z being set st S₂[x1,z] ; :: thesis:

end;

consider f being Function such that
A13: ( dom f = L & ( for z being set st z in L holds
S₂[z,f . z] ) ) from CLASSES1:sch 1(A7);
rng f c= F₃()

proof

let z be set ; :: according to TARSKI:def 3 :: thesis:
assume z in rng f ; :: thesis:
then consider x1 being set such that
A14: ( x1 in dom f & z = f . x1 ) by FUNCT_1:def 5;
x1 in [:F₁(),F₂():] by A5, A13, A14;
then consider x, y being set such that
A15: ( x in F₁() & y in F₂() & x1 = [x,y] ) by ZFMISC_1:def 2;

now

per cases by A5, A13, A14, A15;

suppose A16: P₁[x,y] ; :: thesis:

then f . [x,y] = F₄(x,y) by A13, A14, A15;
hence z in F₃() by A2, A14, A15, A16; :: thesis:

end;

suppose A17: P₂[x,y] ; :: thesis:

then f . [x,y] = F₅(x,y) by A13, A14, A15;
hence z in F₃() by A3, A14, A15, A17; :: thesis:

end;

suppose A18: P₃[x,y] ; :: thesis:

then f . [x,y] = F₆(x,y) by A13, A14, A15;
hence z in F₃() by A4, A14, A15, A18; :: thesis:

end;

hence z in F₃() ; :: thesis:

end;

then reconsider f = f as PartFunc of [:F₁(),F₂():],F₃() by A6, A13, RELSET_1:11;
take f ; :: thesis:
thus for x, y being set holds
( [x,y] in dom f iff ( x in F₁() & y in F₂() & ( P₁[x,y] or P₂[x,y] or P₃[x,y] ) ) ) :: thesis:

proof

let x, y be set ; :: thesis:
thus ( [x,y] in dom f implies ( x in F₁() & y in F₂() & ( P₁[x,y] or P₂[x,y] or P₃[x,y] ) ) ) by A5, A13, ZFMISC_1:106; :: thesis:
assume A19: ( x in F₁() & y in F₂() & ( P₁[x,y] or P₂[x,y] or P₃[x,y] ) ) ; :: thesis:
then A20: [x,y] in [:F₁(),F₂():] by ZFMISC_1:106;

now

let f', r' be set ; :: thesis:
assume [x,y] = [f',r'] ; :: thesis:
then ( x = f' & y = r' ) by ZFMISC_1:33;
hence ( P₁[f',r'] or P₂[f',r'] or P₃[f',r'] ) by A19; :: thesis:

end;

hence [x,y] in dom f by A5, A13, A20; :: thesis:

end;

let x, y be set ; :: thesis:
assume [x,y] in dom f ; :: thesis:
hence ( ( P₁[x,y] implies f . [x,y] = F₄(x,y) ) & ( P₂[x,y] implies f . [x,y] = F₅(x,y) ) & ( P₃[x,y] implies f . [x,y] = F₆(x,y) ) ) by A13; :: thesis: