defpred S1[ object , object ] means ( ( P1[\$1] implies \$2 = F3(\$1) ) & ( P2[\$1] implies \$2 = F4(\$1) ) & ( P3[\$1] implies \$2 = F5(\$1) ) & ( P4[\$1] implies \$2 = F6(\$1) ) );
defpred S2[ object ] means ( P1[\$1] or P2[\$1] or P3[\$1] or P4[\$1] );
consider D being set such that
A6: for x being object holds
( x in D iff ( x in F1() & S2[x] ) ) from A7: for x being object st x in D holds
ex y being object st S1[x,y]
proof
let x be object ; :: thesis: ( x in D implies ex y being object st S1[x,y] )
assume A8: x in D ; :: thesis: ex y being object st S1[x,y]
then A9: x in F1() by A6;
now :: thesis: ex y being set ex y being object st S1[x,y]
per cases ( P1[x] or P2[x] or P3[x] or P4[x] ) by A6, A8;
suppose A10: P1[x] ; :: thesis: ex y being set ex y being object st S1[x,y]
take y = F3(x); :: thesis: ex y being object st S1[x,y]
A11: P4[x] by A1, A9, A10;
( P2[x] & P3[x] ) by A1, A9, A10;
hence ex y being object st S1[x,y] by A11; :: thesis: verum
end;
suppose A12: P2[x] ; :: thesis: ex y being set ex y being object st S1[x,y]
take y = F4(x); :: thesis: ex y being object st S1[x,y]
A13: P4[x] by A1, A9, A12;
( P1[x] & P3[x] ) by A1, A9, A12;
hence ex y being object st S1[x,y] by A13; :: thesis: verum
end;
suppose A14: P3[x] ; :: thesis: ex y being set ex y being object st S1[x,y]
take y = F5(x); :: thesis: ex y being object st S1[x,y]
A15: P4[x] by A1, A9, A14;
( P1[x] & P2[x] ) by A1, A9, A14;
hence ex y being object st S1[x,y] by A15; :: thesis: verum
end;
suppose A16: P4[x] ; :: thesis: ex y being set ex y being object st S1[x,y]
take y = F6(x); :: thesis: ex y being object st S1[x,y]
A17: P3[x] by A1, A9, A16;
( P1[x] & P2[x] ) by A1, A9, A16;
hence ex y being object st S1[x,y] by A17; :: thesis: verum
end;
end;
end;
hence ex y being object st S1[x,y] ; :: thesis: verum
end;
consider f being Function such that
A18: ( dom f = D & ( for x being object st x in D holds
S1[x,f . x] ) ) from A19: D c= F1() by A6;
rng f c= F2()
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in rng f or x in F2() )
assume x in rng f ; :: thesis: x in F2()
then consider y being object such that
A20: y in dom f and
A21: x = f . y by FUNCT_1:def 3;
now :: thesis: x in F2()end;
hence x in F2() ; :: thesis: verum
end;
then reconsider f = f as PartFunc of F1(),F2() by ;
take f ; :: thesis: ( ( for x being object holds
( x in dom f iff ( x in F1() & ( P1[x] or P2[x] or P3[x] or P4[x] ) ) ) ) & ( for x being object st x in dom f holds
( ( P1[x] implies f . x = F3(x) ) & ( P2[x] implies f . x = F4(x) ) & ( P3[x] implies f . x = F5(x) ) & ( P4[x] implies f . x = F6(x) ) ) ) )

thus for x being object holds
( x in dom f iff ( x in F1() & ( P1[x] or P2[x] or P3[x] or P4[x] ) ) ) by ; :: thesis: for x being object st x in dom f holds
( ( P1[x] implies f . x = F3(x) ) & ( P2[x] implies f . x = F4(x) ) & ( P3[x] implies f . x = F5(x) ) & ( P4[x] implies f . x = F6(x) ) )

let x be object ; :: thesis: ( x in dom f implies ( ( P1[x] implies f . x = F3(x) ) & ( P2[x] implies f . x = F4(x) ) & ( P3[x] implies f . x = F5(x) ) & ( P4[x] implies f . x = F6(x) ) ) )
assume x in dom f ; :: thesis: ( ( P1[x] implies f . x = F3(x) ) & ( P2[x] implies f . x = F4(x) ) & ( P3[x] implies f . x = F5(x) ) & ( P4[x] implies f . x = F6(x) ) )
hence ( ( P1[x] implies f . x = F3(x) ) & ( P2[x] implies f . x = F4(x) ) & ( P3[x] implies f . x = F5(x) ) & ( P4[x] implies f . x = F6(x) ) ) by A18; :: thesis: verum