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
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { F2(i) where i is Nat : ( i <= F1() & P1[i] ) } or x in rng f )
assume x in { F2(i) where i is Nat : ( i <= F1() & P1[i] ) } ; :: thesis: x in rng f
then consider j being Nat such that
A3: x = F2(j) and
A4: j <= F1() and
P1[j] ;
 ( 1 <= j + 1 & j + 1 <= F1() + 1 ) by A4, NAT_1:11, XREAL_1:6;
then j + 1 in Seg (F1() + 1) ;
then A5: j + 1 in dom f by A1, Def3;
then f . (j + 1) = F2(((j + 1) - 1)) by A2
.= F2(j) ;
hence x in rng f by A3, A5, FUNCT_1:def 3; :: thesis: verum
end;
hence { F2(i) where i is Nat : ( i <= F1() & P1[i] ) } is finite ; :: thesis: verum