A2:
for k being set st k in F2() holds
ex x being set st
( x in F1() & P1[k,x] )
proof
let k be
set ;
( k in F2() implies ex x being set st
( x in F1() & P1[k,x] ) )
assume A3:
k in F2()
;
ex x being set st
( x in F1() & P1[k,x] )
F2() is
Subset of
NAT
by Th8;
then reconsider k9 =
k as
Element of
NAT by A3;
ex
x being
Element of
F1() st
P1[
k9,
x]
by A1, A3;
hence
ex
x being
set st
(
x in F1() &
P1[
k,
x] )
;
verum
end;
consider f being Function of F2(),F1() such that
A4:
for x being set st x in F2() holds
P1[x,f . x]
from FUNCT_2:sch 1(A2);
dom f = F2()
by FUNCT_2:def 1;
then reconsider p = f as XFinSequence of F1() by AFINSQ_1:7;
take
p
; ( dom p = F2() & ( for k being Nat st k in F2() holds
P1[k,p . k] ) )
thus
( dom p = F2() & ( for k being Nat st k in F2() holds
P1[k,p . k] ) )
by A4, FUNCT_2:def 1; verum