set F = { F₃(i) where i is Element of NAT : ( F₁() <= i & 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 Element of NAT : ( F₁() <= i & i <= F₂() & P₁[i] ) } c= rng f

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in { F₃(i) where i is Element of NAT : ( F₁() <= i & i <= F₂() & P₁[i] ) } or x in rng f )
assume x in { F₃(i) where i is Element of NAT : ( F₁() <= i & i <= F₂() & P₁[i] ) } ; :: thesis: x in rng f
then consider j being Element of NAT such that
A3: x = F₃(j) and
F₁() <= j and
A4: j <= F₂() and
P₁[j] ;
( 1 <= j + 1 & j + 1 <= F₂() + 1 ) by A4, NAT_1:11, XREAL_1:8;
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 5; :: thesis: verum

end;

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