set F = { F₂(i) where i is Nat : ( i <= F₁() & P₁[i] ) } ;
deffunc H₁( Nat) -> set = F₂(($1 - 1));
consider f being FinSequence such that
A1: len f = F₁() + 1 and
A2: for k being Nat st k in dom f holds
f . k = H₁(k) from FINSEQ_1:sch 2();
{ F₂(i) where i is Nat : ( i <= F₁() & P₁[i] ) } c= rng f

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { F₂(i) where i is Nat : ( i <= F₁() & P₁[i] ) } or x in rng f )
assume x in { F₂(i) where i is Nat : ( i <= F₁() & P₁[i] ) } ; :: thesis: x in rng f
then consider j being Nat such that
A3: x = F₂(j) and
A4: j <= F₁() and
P₁[j] ;
( 1 <= j + 1 & j + 1 <= F₁() + 1 ) by A4, NAT_1:11, XREAL_1:6;
then j + 1 in Seg (F₁() + 1) ;
then A5: j + 1 in dom f by A1, Def3;
then f . (j + 1) = F₂(((j + 1) - 1)) by A2
.= F₂(j) ;
hence x in rng f by A3, A5, FUNCT_1:def 3; :: thesis: verum

end;

hence { F₂(i) where i is Nat : ( i <= F₁() & P₁[i] ) } is finite ; :: thesis: verum