defpred S₁[ object , object ] 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₂[ object ] means ( P₁[$1] or P₂[$1] or P₃[$1] or P₄[$1] );
consider B being set such that
A2: for x being object holds
( x in B iff ( x in F₁() & S₂[x] ) ) from XBOOLE_0:sch 1();
A3: for x being object st x in B holds
ex y being object st S₁[x,y]

let x be object ; :: thesis:
assume A4: x in B ; :: thesis:
then reconsider e9 = x as Element of F₁() by A2;

per cases by A2, A4;

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

take y = F₃(x); :: thesis:
A6: P₄[e9] by A1, A5;
( P₂[e9] & P₃[e9] ) by A1, A5;
hence ex y being object st S₁[x,y] by A6; :: thesis:

end;

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

take y = F₄(x); :: thesis:
A8: P₄[e9] by A1, A7;
( P₁[e9] & P₃[e9] ) by A1, A7;
hence ex y being object st S₁[x,y] by A8; :: thesis:

end;

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

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

end;

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

take y = F₆(x); :: thesis:
A12: P₃[e9] by A1, A11;
( P₁[e9] & P₂[e9] ) by A1, A11;
hence ex y being object st S₁[x,y] by A12; :: thesis:

end;

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

end;

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

proof

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

now :: thesis:

per cases by A2, A13, A15;

suppose P₁[y] ; :: thesis:

then f . y = F₃(y) by A13, A15;
hence x in F₂() by A16; :: thesis:

end;

suppose P₂[y] ; :: thesis:

then f . y = F₄(y) by A13, A15;
hence x in F₂() by A16; :: thesis:

end;

suppose P₃[y] ; :: thesis:

then f . y = F₅(y) by A13, A15;
hence x in F₂() by A16; :: thesis:

end;

suppose P₄[y] ; :: thesis:

then f . y = F₆(y) by A13, A15;
hence x in F₂() by A16; :: thesis:

end;

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

end;

B c= F₁() by A2;
then reconsider q = f as PartFunc of F₁(),F₂() by A13, A14, RELSET_1:4;
take q ; :: thesis:
thus for c being Element of F₁() holds
( c in dom q iff ( P₁[c] or P₂[c] or P₃[c] or P₄[c] ) ) by A2, A13; :: thesis:
let o be Element of F₁(); :: thesis:
assume o in dom q ; :: thesis:
hence ( ( P₁[o] implies q . o = F₃(o) ) & ( P₂[o] implies q . o = F₄(o) ) & ( P₃[o] implies q . o = F₅(o) ) & ( P₄[o] implies q . o = F₆(o) ) ) by A13; :: thesis: