defpred S₁[ object , object ] means for x, y being object 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) ) );
defpred S₂[ object ] means for x, y being object 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 object holds
( z in L iff ( z in [:F₁(),F₂():] & S₂[z] ) ) from XBOOLE_0:sch 1();
A6: for x1 being object st x1 in L holds
ex z being object st S₁[x1,z]

let x1 be object ; :: thesis:
assume A7: x1 in L ; :: thesis:
then x1 in [:F₁(),F₂():] by A5;
then consider z9, a9 being object such that
A8: ( z9 in F₁() & a9 in F₂() ) and
A9: x1 = [z9,a9] by ZFMISC_1:def 2;

per cases by A5, A7, A9;

suppose A10: P₁[z9,a9] ; :: thesis:

take z = F₄(z9,a9); :: thesis:
let x, y be object ; :: thesis:
assume x1 = [x,y] ; :: thesis:
then ( z9 = x & a9 = y ) by A9, XTUPLE_0:1;
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, A8, A10; :: thesis:

end;

suppose A11: P₂[z9,a9] ; :: thesis:

take z = F₅(z9,a9); :: thesis:
let x, y be object ; :: thesis:
assume x1 = [x,y] ; :: thesis:
then ( z9 = x & a9 = y ) by A9, XTUPLE_0:1;
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, A8, A11; :: thesis:

end;

suppose A12: P₃[z9,a9] ; :: thesis:

take z = F₆(z9,a9); :: thesis:
let x, y be object ; :: thesis:
assume x1 = [x,y] ; :: thesis:
then ( z9 = x & a9 = y ) by A9, XTUPLE_0:1;
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, A8, A12; :: thesis:

end;

hence ex z being object st S₁[x1,z] ; :: thesis:

end;

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

proof

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

now :: thesis:

per cases by A5, A13, A15, A18;

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

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

end;

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

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

end;

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

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

end;

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

end;

L c= [:F₁(),F₂():] by A5;
then reconsider f = f as PartFunc of [:F₁(),F₂():],F₃() by A13, A14, RELSET_1:4;
take f ; :: thesis:
thus for x, y being object 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 object ; :: 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:87; :: thesis:
assume that
A22: ( x in F₁() & y in F₂() ) and
A23: ( P₁[x,y] or P₂[x,y] or P₃[x,y] ) ; :: thesis:

A24: now :: thesis:

let f9, r9 be object ; :: thesis:
assume A25: [x,y] = [f9,r9] ; :: thesis:
then x = f9 by XTUPLE_0:1;
hence ( P₁[f9,r9] or P₂[f9,r9] or P₃[f9,r9] ) by A23, A25, XTUPLE_0:1; :: thesis:

end;

[x,y] in [:F₁(),F₂():] by A22, ZFMISC_1:87;
hence [x,y] in dom f by A5, A13, A24; :: thesis:

end;

let x, y be object ; :: 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: