defpred S1[ object ] means ex c being Element of F2() st P1[$1,c];
set x = the Element of F2();
defpred S2[ object , object ] means ( ( ex c being Element of F2() st P1[$1,c] implies P1[$1,$2] ) & ( ( for c being Element of F2() holds P1[$1,c] ) implies $2 = the Element of F2() ) );
consider X being set such that
A1:
for x being object holds
( x in X iff ( x in F1() & S1[x] ) )
from XBOOLE_0:sch 1();
for x being object st x in X holds
x in F1()
by A1;
then reconsider X = X as Subset of F1() by TARSKI:def 3;
A2:
for d being Element of F1() ex z being Element of F2() st S2[d,z]
proof
let d be
Element of
F1();
ex z being Element of F2() st S2[d,z]
( ( for
c being
Element of
F2() holds
P1[
d,
c] ) implies ex
z being
Element of
F2() st
( ( ex
c being
Element of
F2() st
P1[
d,
c] implies
P1[
d,
z] ) & ( ( for
c being
Element of
F2() holds
P1[
d,
c] ) implies
z = the
Element of
F2() ) ) )
;
hence
ex
z being
Element of
F2() st
S2[
d,
z]
;
verum
end;
consider g being Function of F1(),F2() such that
A3:
for d being Element of F1() holds S2[d,g . d]
from FUNCT_2:sch 3(A2);
reconsider f = g | X as PartFunc of F1(),F2() ;
take
f
; ( ( for d being Element of F1() holds
( d in dom f iff ex c being Element of F2() st P1[d,c] ) ) & ( for d being Element of F1() st d in dom f holds
P1[d,f /. d] ) )
A4:
dom g = F1()
by FUNCT_2:def 1;
thus
for d being Element of F1() holds
( d in dom f iff ex c being Element of F2() st P1[d,c] )
for d being Element of F1() st d in dom f holds
P1[d,f /. d]
let d be Element of F1(); ( d in dom f implies P1[d,f /. d] )
assume A5:
d in dom f
; P1[d,f /. d]
dom f c= X
by RELAT_1:58;
then
ex c being Element of F2() st P1[d,c]
by A1, A5;
then
P1[d,g . d]
by A3;
then
P1[d,f . d]
by A5, FUNCT_1:47;
hence
P1[d,f /. d]
by A5, PARTFUN1:def 6; verum