A2: for k being set st k in F₂() holds
ex x being set st
( x in F₁() & P₁[k,x] )

proof

let k be set ; :: thesis: ( k in F₂() implies ex x being set st
( x in F₁() & P₁[k,x] ) )
assume A3: k in F₂() ; :: thesis: ex x being set st
( x in F₁() & P₁[k,x] )
F₂() is Subset of NAT by Th8;
then reconsider k' = k as Element of NAT by A3;
ex x being Element of F₁() st P₁[k',x] by A1, A3;
hence ex x being set st
( x in F₁() & P₁[k,x] ) ; :: thesis: verum

end;

consider f being Function of F₂(),F₁() such that
A4: for x being set st x in F₂() holds
P₁[x,f . x] from FUNCT_2:sch 1(A2);
( rng f c= F₁() & dom f = F₂() ) by FUNCT_2:def 1;
then reconsider p = f as XFinSequence of by AFINSQ_1:7;
take p ; :: thesis: ( dom p = F₂() & ( for k being Element of NAT st k in F₂() holds
P₁[k,p . k] ) )
thus ( dom p = F₂() & ( for k being Element of NAT st k in F₂() holds
P₁[k,p . k] ) ) by A4, FUNCT_2:def 1; :: thesis: verum