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

proof

let x be object ; :: thesis: ( x in S implies ex y being object st S₁[x,y] )
assume A7: x in S ; :: thesis: ex y being object st S₁[x,y]
then A8: x in F₁() by A5;

now :: thesis: ex y being set ex y being object st S₁[x,y]

per cases ( P₁[x] or P₂[x] or P₃[x] ) by A5, A7;

suppose A9: P₁[x] ; :: thesis: ex y being set ex y being object st S₁[x,y]

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

end;

suppose A10: P₂[x] ; :: thesis: ex y being set ex y being object st S₁[x,y]

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

end;

suppose A11: P₃[x] ; :: thesis: ex y being set ex y being object st S₁[x,y]

take y = F₅(x); :: thesis: ex y being object st S₁[x,y]
( P₁[x] & P₂[x] ) by A1, A8, A11;
hence ex y being object st S₁[x,y] ; :: thesis: verum

end;

end;

end;

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

end;

consider f being Function such that
A12: ( dom f = S & ( for x being object st x in S holds
S₁[x,f . x] ) ) from CLASSES1:sch 1(A6);
A13: S c= F₁() by A5;
rng f c= F₂()

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in rng f or x in F₂() )
assume x in rng f ; :: thesis: x in F₂()
then consider y being object such that
A14: y in dom f and
A15: x = f . y by FUNCT_1:def 3;

now :: thesis: x in F₂()

per cases ( P₁[y] or P₂[y] or P₃[y] ) by A5, A12, A14;

suppose A16: P₁[y] ; :: thesis: x in F₂()

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

end;

suppose A17: P₂[y] ; :: thesis: x in F₂()

then f . y = F₄(y) by A12, A14;
hence x in F₂() by A3, A13, A12, A14, A15, A17; :: thesis: verum

end;

suppose A18: P₃[y] ; :: thesis: x in F₂()

then f . y = F₅(y) by A12, A14;
hence x in F₂() by A4, A13, A12, A14, A15, A18; :: thesis: verum

end;

end;

end;

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

end;

then reconsider f = f as PartFunc of F₁(),F₂() by A13, A12, RELSET_1:4;
take f ; :: thesis: ( ( for x being object holds
( x in dom f iff ( x in F₁() & ( P₁[x] or P₂[x] or P₃[x] ) ) ) ) & ( for x being object st x in dom f holds
( ( P₁[x] implies f . x = F₃(x) ) & ( P₂[x] implies f . x = F₄(x) ) & ( P₃[x] implies f . x = F₅(x) ) ) ) )
thus for x being object holds
( x in dom f iff ( x in F₁() & ( P₁[x] or P₂[x] or P₃[x] ) ) ) by A5, A12; :: thesis: for x being object st x in dom f holds
( ( P₁[x] implies f . x = F₃(x) ) & ( P₂[x] implies f . x = F₄(x) ) & ( P₃[x] implies f . x = F₅(x) ) )
let x be object ; :: thesis: ( x in dom f implies ( ( P₁[x] implies f . x = F₃(x) ) & ( P₂[x] implies f . x = F₄(x) ) & ( P₃[x] implies f . x = F₅(x) ) ) )
assume x in dom f ; :: thesis: ( ( P₁[x] implies f . x = F₃(x) ) & ( P₂[x] implies f . x = F₄(x) ) & ( P₃[x] implies f . x = F₅(x) ) )
hence ( ( P₁[x] implies f . x = F₃(x) ) & ( P₂[x] implies f . x = F₄(x) ) & ( P₃[x] implies f . x = F₅(x) ) ) by A12; :: thesis: verum