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 A being set such that
A4:
for x being object holds
( x in A iff ( x in F1() & S2[x] ) )
from XBOOLE_0:sch 1();
A5:
for x being object st x in A holds
ex y being object st S1[x,y]
proof
let x be
object ;
( x in A implies ex y being object st S1[x,y] )
assume A6:
x in A
;
ex y being object st S1[x,y]
then A7:
x in F1()
by A4;
now ex y being set ex y being object st S1[x,y]per cases
( P1[x] or P2[x] )
by A4, A6;
suppose A8:
P1[
x]
;
ex y being set ex y being object st S1[x,y]take y =
F3(
x);
ex y being object st S1[x,y]
P2[
x]
by A1, A7, A8;
hence
ex
y being
object st
S1[
x,
y]
;
verum end; suppose A9:
P2[
x]
;
ex y being set ex y being object st S1[x,y]take y =
F4(
x);
ex y being object st S1[x,y]
P1[
x]
by A1, A7, A9;
hence
ex
y being
object st
S1[
x,
y]
;
verum end; end; end;
hence
ex
y being
object st
S1[
x,
y]
;
verum
end;
consider f being Function such that
A10:
( dom f = A & ( for x being object st x in A holds
S1[x,f . x] ) )
from CLASSES1:sch 1(A5);
A11:
A c= F1()
by A4;
rng f c= F2()
then reconsider f = f as PartFunc of F1(),F2() by A11, A10, RELSET_1:4;
take
f
; ( ( for x being object holds
( x in dom f iff ( x in F1() & ( P1[x] or P2[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) ) ) ) )
thus
for x being object holds
( x in dom f iff ( x in F1() & ( P1[x] or P2[x] ) ) )
by A4, A10; for x being object st x in dom f holds
( ( P1[x] implies f . x = F3(x) ) & ( P2[x] implies f . x = F4(x) ) )
let x be object ; ( x in dom f implies ( ( P1[x] implies f . x = F3(x) ) & ( P2[x] implies f . x = F4(x) ) ) )
assume
x in dom f
; ( ( P1[x] implies f . x = F3(x) ) & ( P2[x] implies f . x = F4(x) ) )
hence
( ( P1[x] implies f . x = F3(x) ) & ( P2[x] implies f . x = F4(x) ) )
by A10; verum