defpred S2[ set , set ] means for y being set holds
( y in $2 iff ( y in F2($1) & P1[$1,y] ) );
A1:
for x being set st x in F1() holds
ex y being set st S2[x,y]
proof
let x be
set ;
( x in F1() implies ex y being set st S2[x,y] )
assume
x in F1()
;
ex y being set st S2[x,y]
defpred S3[
set ]
means P1[
x,$1];
consider Y being
set such that A2:
for
y being
set holds
(
y in Y iff (
y in F2(
x) &
S3[
y] ) )
from XBOOLE_0:sch 1();
take
Y
;
S2[x,Y]
thus
S2[
x,
Y]
by A2;
verum
end;
thus
ex f being Function st
( dom f = F1() & ( for x being set st x in F1() holds
S2[x,f . x] ) )
from CLASSES1:sch 1(A1); verum