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

proof

let y be set ; :: thesis: ( y in Seg F₂() implies ex x being set st
( x in F₁() & P₁[y,x] ) )
assume A3: y in Seg F₂() ; :: thesis: ex x being set st
( x in F₁() & P₁[y,x] )
then reconsider k = y as Element of NAT ;
consider x being Element of F₁() such that
A4: P₁[k,x] by A1, A3;
take x ; :: thesis: ( x in F₁() & P₁[y,x] )
thus ( x in F₁() & P₁[y,x] ) by A4; :: thesis: verum

end;

consider f being Function such that
A5: dom f = Seg F₂() and
A6: rng f c= F₁() and
A7: for y being set st y in Seg F₂() holds
P₁[y,f . y] from WELLORD2:sch 1(A2);
reconsider f = f as FinSequence by A5, Def2;
reconsider p = f as FinSequence of F₁() by A6, Def4;
take p ; :: thesis: ( dom p = Seg F₂() & ( for k being Nat st k in Seg F₂() holds
P₁[k,p . k] ) )
thus ( dom p = Seg F₂() & ( for k being Nat st k in Seg F₂() holds
P₁[k,p . k] ) ) by A5, A7; :: thesis: verum