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

proof

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

end;

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