reconsider X = F₁() as set ;
defpred S₁[ set , set ] means ( P₁[$1,$2] & $2 in F₁() );

A2: now

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

end;

consider f being Function such that
A5: ( dom f = Seg F₂() & rng f c= X & ( for x being set st x in Seg F₂() holds
S₁[x,f . x] ) ) from WELLORD2:sch 1(A2);
reconsider f = f as FinSequence by A5, FINSEQ_1:def 2;
reconsider f = f as FinSequence of F₁() by A5, FINSEQ_1:def 4;
take f ; :: thesis: ( len f = F₂() & ( for n being Nat st n in Seg F₂() holds
P₁[n,f /. n] ) )
F₂() in NAT by ORDINAL1:def 13;
hence len f = F₂() by A5, FINSEQ_1:def 3; :: thesis: for n being Nat st n in Seg F₂() holds
P₁[n,f /. n]
let n be Nat; :: thesis: ( n in Seg F₂() implies P₁[n,f /. n] )
assume A6: n in Seg F₂() ; :: thesis: P₁[n,f /. n]
then P₁[n,f . n] by A5;
hence P₁[n,f /. n] by A5, A6, PARTFUN1:def 8; :: thesis: verum