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

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

per cases by A2, A4;

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

take y = F₃(d9); :: thesis:

now :: thesis:

per cases ;

suppose A6: P₂[d9] ; :: thesis:

then A7: F₃(d9) = F₄(d9) by A1, A5;

now :: thesis:

per cases ;

suppose P₃[d9] ; :: thesis:

then F₄(d9) = F₅(d9) by A1, A6;
hence ex y being object st S₁[x,y] by A7; :: thesis:

end;

suppose P₃[d9] ; :: thesis:

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

end;

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

end;

suppose A8: P₂[d9] ; :: thesis:

now :: thesis:

per cases ;

suppose P₃[d9] ; :: thesis:

then F₃(d9) = F₅(d9) by A1, A5;
hence ex y being object st S₁[x,y] by A8; :: thesis:

end;

suppose P₃[d9] ; :: thesis:

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

end;

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

end;

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

end;

suppose A9: P₂[d9] ; :: thesis:

take y = F₄(x); :: thesis:

now :: thesis:

per cases ;

suppose P₁[d9] ; :: thesis:

then A10: F₃(d9) = F₄(d9) by A1, A9;

now :: thesis:

per cases ;

suppose P₃[d9] ; :: thesis:

then F₄(d9) = F₅(d9) by A1, A9;
hence ex y being object st S₁[x,y] by A10; :: thesis:

end;

suppose P₃[d9] ; :: thesis:

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

end;

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

end;

suppose A11: P₁[d9] ; :: thesis:

now :: thesis:

per cases ;

suppose P₃[d9] ; :: thesis:

then F₄(d9) = F₅(d9) by A1, A9;
hence ex y being object st S₁[x,y] by A11; :: thesis:

end;

suppose P₃[d9] ; :: thesis:

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

end;

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

end;

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

end;

suppose A12: P₃[d9] ; :: thesis:

take y = F₅(x); :: thesis:

now :: thesis:

per cases ;

suppose P₁[d9] ; :: thesis:

then A13: F₃(d9) = F₅(d9) by A1, A12;

now :: thesis:

per cases ;

suppose P₂[d9] ; :: thesis:

then F₄(d9) = F₅(d9) by A1, A12;
hence ex y being object st S₁[x,y] by A13; :: thesis:

end;

suppose P₂[d9] ; :: thesis:

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

end;

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

end;

suppose A14: P₁[d9] ; :: thesis:

now :: thesis:

per cases ;

suppose P₂[d9] ; :: thesis:

then F₄(d9) = F₅(d9) by A1, A12;
hence ex y being object st S₁[x,y] by A14; :: thesis:

end;

suppose P₂[d9] ; :: thesis:

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

end;

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

end;

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

end;

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

end;

consider f being Function such that
A15: ( dom f = V & ( for x being object st x in V holds
S₁[x,f . x] ) ) from CLASSES1:sch 1(A3);
A16: 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
A17: y in dom f and
A18: x = f . y by FUNCT_1:def 3;

now :: thesis:

per cases by A2, A15, A17;

suppose P₁[y] ; :: thesis:

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

end;

suppose P₂[y] ; :: thesis:

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

end;

suppose P₃[y] ; :: thesis:

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

end;

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

end;

V c= F₁() by A2;
then reconsider q = f as PartFunc of F₁(),F₂() by A15, A16, 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] ) ) by A2, A15; :: thesis:
let i be Element of F₁(); :: thesis:
assume i in dom q ; :: thesis:
hence ( ( P₁[i] implies q . i = F₃(i) ) & ( P₂[i] implies q . i = F₄(i) ) & ( P₃[i] implies q . i = F₅(i) ) ) by A15; :: thesis: