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 B being set such that
A2: for x being object holds
( x in B iff ( x in F1() & S2[x] ) ) from A3: for x being object st x in B holds
ex y being object st S1[x,y]
proof
let x be object ; :: thesis: ( x in B implies ex y being object st S1[x,y] )
assume A4: x in B ; :: thesis: ex y being object st S1[x,y]
then reconsider e9 = x as Element of F1() by A2;
now :: thesis: ex y being Element of F2() ex y being object st S1[x,y]
per cases ( P1[x] or P2[x] or P3[x] or P4[x] ) by A2, A4;
suppose A5: P1[x] ; :: thesis: ex y being Element of F2() ex y being object st S1[x,y]
take y = F3(x); :: thesis: ex y being object st S1[x,y]
A6: P4[e9] by A1, A5;
( P2[e9] & P3[e9] ) by A1, A5;
hence ex y being object st S1[x,y] by A6; :: thesis: verum
end;
suppose A7: P2[x] ; :: thesis: ex y being Element of F2() ex y being object st S1[x,y]
take y = F4(x); :: thesis: ex y being object st S1[x,y]
A8: P4[e9] by A1, A7;
( P1[e9] & P3[e9] ) by A1, A7;
hence ex y being object st S1[x,y] by A8; :: thesis: verum
end;
suppose A9: P3[x] ; :: thesis: ex y being Element of F2() ex y being object st S1[x,y]
take y = F5(x); :: thesis: ex y being object st S1[x,y]
A10: P4[e9] by A1, A9;
( P1[e9] & P2[e9] ) by A1, A9;
hence ex y being object st S1[x,y] by A10; :: thesis: verum
end;
suppose A11: P4[x] ; :: thesis: ex y being Element of F2() ex y being object st S1[x,y]
take y = F6(x); :: thesis: ex y being object st S1[x,y]
A12: P3[e9] by A1, A11;
( P1[e9] & P2[e9] ) by A1, A11;
hence ex y being object st S1[x,y] by A12; :: thesis: verum
end;
end;
end;
hence ex y being object st S1[x,y] ; :: thesis: verum
end;
consider f being Function such that
A13: ( dom f = B & ( for y being object st y in B holds
S1[y,f . y] ) ) from A14: 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
A15: y in dom f and
A16: x = f . y by FUNCT_1:def 3;
now :: thesis: x in F2()end;
hence x in F2() ; :: thesis: verum
end;
B c= F1() by A2;
then reconsider q = f as PartFunc of F1(),F2() by ;
take q ; :: thesis: ( ( for c being Element of F1() holds
( c in dom q iff ( P1[c] or P2[c] or P3[c] or P4[c] ) ) ) & ( for c being Element of F1() st c in dom q holds
( ( P1[c] implies q . c = F3(c) ) & ( P2[c] implies q . c = F4(c) ) & ( P3[c] implies q . c = F5(c) ) & ( P4[c] implies q . c = F6(c) ) ) ) )

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

let o be Element of F1(); :: thesis: ( o in dom q implies ( ( P1[o] implies q . o = F3(o) ) & ( P2[o] implies q . o = F4(o) ) & ( P3[o] implies q . o = F5(o) ) & ( P4[o] implies q . o = F6(o) ) ) )
assume o in dom q ; :: thesis: ( ( P1[o] implies q . o = F3(o) ) & ( P2[o] implies q . o = F4(o) ) & ( P3[o] implies q . o = F5(o) ) & ( P4[o] implies q . o = F6(o) ) )
hence ( ( P1[o] implies q . o = F3(o) ) & ( P2[o] implies q . o = F4(o) ) & ( P3[o] implies q . o = F5(o) ) & ( P4[o] implies q . o = F6(o) ) ) by A13; :: thesis: verum