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

proof

let x be object ; :: thesis: ( x in Z implies ex y being object st S₁[x,y] )
assume A4: x in Z ; :: thesis: ex y being object st S₁[x,y]
then reconsider c9 = x as Element of F₁() by A2;

now :: thesis: ex y being Element of F₂() ex y being object st S₁[x,y]

per cases ( P₁[x] or P₂[x] or P₃[x] ) by A2, A4;

suppose A5: P₁[x] ; :: thesis: ex y being Element of F₂() ex y being object st S₁[x,y]

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

end;

suppose A6: P₂[x] ; :: thesis: ex y being Element of F₂() ex y being object st S₁[x,y]

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

end;

suppose A7: P₃[x] ; :: thesis: ex y being Element of F₂() ex y being object st S₁[x,y]

take y = F₅(x); :: thesis: ex y being object st S₁[x,y]
( P₁[c9] & P₂[c9] ) by A1, A7;
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
A8: ( dom f = Z & ( for x being object st x in Z holds
S₁[x,f . x] ) ) from CLASSES1:sch 1(A3);
A9: 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
A10: y in dom f and
A11: x = f . y by FUNCT_1:def 3;

now :: thesis: x in F₂()

per cases ( P₁[y] or P₂[y] or P₃[y] ) by A2, A8, A10;

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

then f . y = F₃(y) by A8, A10;
hence x in F₂() by A11; :: thesis: verum

end;

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

then f . y = F₄(y) by A8, A10;
hence x in F₂() by A11; :: thesis: verum

end;

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

then f . y = F₅(y) by A8, A10;
hence x in F₂() by A11; :: thesis: verum

end;

end;

end;

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

end;

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