defpred S1[ object , object ] means ( ( P1[$1] implies $2 = F3($1) ) & ( P2[$1] implies $2 = F4($1) ) );
defpred S2[ object ] means ( P1[$1] or P2[$1] );
consider X being set such that
A2: for x being object holds
( x in X iff ( x in F1() & S2[x] ) ) from XBOOLE_0:sch 1();
 A3: for x being object st x in X holds
ex y being object st S1[x,y]
proof
let x be object ; :: thesis: ( x in X implies ex y being object st S1[x,y] )
assume A4: x in X ; :: thesis: ex y being object st S1[x,y]
then reconsider x9 = 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] ) 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]
P2[x9] by A1, A5;
hence ex y being object st S1[x,y] ; :: thesis: verum
end;
suppose A6: 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]
P1[x9] by A1, A6;
hence ex y being object st S1[x,y] ; :: thesis: verum
end;
end;
end;
hence ex y being object st S1[x,y] ; :: thesis: verum
end;
consider f being Function such that
A7: ( dom f = X & ( for x being object st x in X holds
S1[x,f . x] ) ) from CLASSES1:sch 1(A3);
 A8: X c= F1() by A2;
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
A9: y in dom f and
A10: x = f . y by FUNCT_1:def 3;
now :: thesis: x in F2()
end;
hence x in F2() ; :: thesis: verum
end;
then reconsider q = f as PartFunc of F1(),F2() by A8, A7, RELSET_1:4;
take q ; :: thesis: ( ( for c being Element of F1() holds
( c in dom q iff ( P1[c] or P2[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) ) ) ) )
thus for c being Element of F1() holds
( c in dom q iff ( P1[c] or P2[c] ) ) by A2, A7; :: 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) ) )
let b be Element of F1(); :: thesis: ( b in dom q implies ( ( P1[b] implies q . b = F3(b) ) & ( P2[b] implies q . b = F4(b) ) ) )
assume b in dom q ; :: thesis: ( ( P1[b] implies q . b = F3(b) ) & ( P2[b] implies q . b = F4(b) ) )
hence ( ( P1[b] implies q . b = F3(b) ) & ( P2[b] implies q . b = F4(b) ) ) by A7; :: thesis: verum