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