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

A2: now :: thesis: for x being object st x in Seg F₂() holds
ex y being object st
( y in X & S₁[x,y] )

let x be object ; :: thesis: ( x in Seg F₂() implies ex y being object st
( y in X & S₁[x,y] ) )
assume A3: x in Seg F₂() ; :: thesis: ex y being object st
( y in X & S₁[x,y] )
then reconsider x9 = x as Element of NAT ;
consider d being Element of F₁() such that
A4: P₁[x9,d] by A1, A3;
reconsider y = d as object ;
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 object st x in Seg F₂() holds
S₁[x,f . x] ) ) from FUNCT_1:sch 6(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 12;
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 6; :: thesis: verum