defpred S₁[ set , set ] means ( ( P₁[$1] implies $2 = F₃($1) ) & ( P₂[$1] implies $2 = F₄($1) ) & ( P₃[$1] implies $2 = F₅($1) ) & ( P₄[$1] implies $2 = F₆($1) ) );
defpred S₂[ set ] means ( P₁[$1] or P₂[$1] or P₃[$1] or P₄[$1] );
consider D being set such that
A6: for x being set holds
( x in D iff ( x in F₁() & S₂[x] ) ) from XBOOLE_0:sch 1();
A7: for x being set st x in D holds
ex y being set st S₁[x,y]

let x be set ; :: thesis:
assume A8: x in D ; :: thesis:
then A9: x in F₁() by A6;

per cases by A6, A8;

suppose A10: P₁[x] ; :: thesis:

take y = F₃(x); :: thesis:
A11: P₄[x] by A1, A9, A10;
( P₂[x] & P₃[x] ) by A1, A9, A10;
hence ex y being set st S₁[x,y] by A11; :: thesis:

end;

suppose A12: P₂[x] ; :: thesis:

take y = F₄(x); :: thesis:
A13: P₄[x] by A1, A9, A12;
( P₁[x] & P₃[x] ) by A1, A9, A12;
hence ex y being set st S₁[x,y] by A13; :: thesis:

end;

suppose A14: P₃[x] ; :: thesis:

take y = F₅(x); :: thesis:
A15: P₄[x] by A1, A9, A14;
( P₁[x] & P₂[x] ) by A1, A9, A14;
hence ex y being set st S₁[x,y] by A15; :: thesis:

end;

suppose A16: P₄[x] ; :: thesis:

take y = F₆(x); :: thesis:
A17: P₃[x] by A1, A9, A16;
( P₁[x] & P₂[x] ) by A1, A9, A16;
hence ex y being set st S₁[x,y] by A17; :: thesis:

end;

hence ex y being set st S₁[x,y] ; :: thesis:

end;

consider f being Function such that
A18: ( dom f = D & ( for x being set st x in D holds
S₁[x,f . x] ) ) from CLASSES1:sch 1(A7);
A19: D c= F₁()

proof

let x be set ; :: according to TARSKI:def 3 :: thesis:
assume x in D ; :: thesis:
hence x in F₁() by A6; :: thesis:

end;

rng f c= F₂()

proof

let x be set ; :: according to TARSKI:def 3 :: thesis:
assume x in rng f ; :: thesis:
then consider y being set such that
A20: y in dom f and
A21: x = f . y by FUNCT_1:def 3;

now

per cases by A6, A18, A20;

suppose A22: P₁[y] ; :: thesis:

then f . y = F₃(y) by A18, A20;
hence x in F₂() by A2, A19, A18, A20, A21, A22; :: thesis:

end;

suppose A23: P₂[y] ; :: thesis:

then f . y = F₄(y) by A18, A20;
hence x in F₂() by A3, A19, A18, A20, A21, A23; :: thesis:

end;

suppose A24: P₃[y] ; :: thesis:

then f . y = F₅(y) by A18, A20;
hence x in F₂() by A4, A19, A18, A20, A21, A24; :: thesis:

end;

suppose A25: P₄[y] ; :: thesis:

then f . y = F₆(y) by A18, A20;
hence x in F₂() by A5, A19, A18, A20, A21, A25; :: thesis:

end;

hence x in F₂() ; :: thesis:

end;

then reconsider f = f as PartFunc of F₁(),F₂() by A19, A18, RELSET_1:4;
take f ; :: thesis:
thus for x being set holds
( x in dom f iff ( x in F₁() & ( P₁[x] or P₂[x] or P₃[x] or P₄[x] ) ) ) by A6, A18; :: thesis:
let x be set ; :: thesis:
assume x in dom f ; :: thesis:
hence ( ( P₁[x] implies f . x = F₃(x) ) & ( P₂[x] implies f . x = F₄(x) ) & ( P₃[x] implies f . x = F₅(x) ) & ( P₄[x] implies f . x = F₆(x) ) ) by A18; :: thesis: